AV视频

Foundations of Software Systems (FoSS)

Peter Schrammel

Selected Publications

2023

  • Mal铆k, V., Ne膷as, F., Schrammel, P., & Vojnar, T. (2023). 2LS: Arrays and Loop Unwinding. In Lecture Notes in Computer Science (pp. 529-534). Springer Nature Switzerland. doi:10.1007/978-3-031-30820-8_31
    Chapter. .
  • G眉demann, M., & Schrammel, P. (2023). BlueCov: Integrating Test Coverage and Model Checking with JBMC. In Proceedings of the ACM Symposium on Applied Computing (pp. 1695-1697). doi:10.1145/3555776.3577829
    Conference publication. .
  • Kroening, D., Schrammel, P., & Tautschnig, M. (2023). CBMC: The C Bounded Model Checker. Retrieved from http://arxiv.org/abs/2302.02384v1
    Preprint.
  • Kroening, D., Mal铆k, V., Schrammel, P., & Vojnar, T. (2023). 2LS for Program Analysis. Retrieved from http://arxiv.org/abs/2302.02380v1
    Preprint.
  • Brenguier, R., Cordeiro, L., Kroening, D., & Schrammel, P. (2023). JBMC: A Bounded Model Checking Tool for Java Bytecode. Retrieved from http://arxiv.org/abs/2302.02381v1
    Preprint.
  • Mal铆k, V., Ne膷as, F., Schrammel, P., & Vojnar, T. (2023). 2LS: Arrays and Loop Unwinding: (Competition Contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 13994 LNCS (pp. 529-534). doi:10.1007/978-3-031-30820-8_31
    Conference publication. .

2022

  • G眉demann, M., & Schrammel, P. (2022). BlueCov: Integrating Test Coverage and Model Checking with JBMC. Retrieved from http://arxiv.org/abs/2212.14779v1
    Preprint.
  • Fischer, B., La Torre, S., Parlato, G., & Schrammel, P. (2022). CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory. In ACM International Conference Proceeding Series. doi:10.1145/3551349.3559523
    Conference publication. .
  • Wu, T., Schrammel, P., & Cordeiro, L. C. (2022). Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). In Unknown Book (Vol. 13244 LNCS, pp. 484-489). doi:10.1007/978-3-030-99527-0_36
    Chapter. .

2021

  • Cattaruzza, D., Abate, A., Schrammel, P., & Kroening, D. (2021). Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. Journal of Automated Reasoning, 65(2), 157-203. doi:10.1007/s10817-020-09562-z
    Article. .

2020

  • Schrammel, P. (2020). How Testable is Business Software?. Retrieved from http://arxiv.org/abs/2011.00630v1
    Preprint.
  • Schrammel, P. (2020). The FMCAD 2020 Student Forum. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020. doi:10.34727/2020/isbn.978-3-85448-042-6_6
    Conference publication. .
  • Mal铆k, V., Schrammel, P., & Vojnar, T. (2020). 2LS: Heap Analysis and Memory Safety. In Lecture Notes in Computer Science (pp. 368-372). Springer International Publishing. doi:10.1007/978-3-030-45237-7_22
    Chapter. .
  • Duggirala, P. S., & Schrammel, P. (2020). NSV 2020 Preface (Vol. 12549 LNCS).
    Book.
  • Mal铆k, V., Schrammel, P., & Vojnar, T. (2020). 2LS: Heap Analysis and Memory Safety: (Competition Contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 12079 LNCS (pp. 368-372). doi:10.1007/978-3-030-45237-7_22
    Conference publication. .

2019

  • Cordeiro, L., Kroening, D., & Schrammel, P. (2019). JBMC: Bounded Model Checking for Java Bytecode. In Lecture Notes in Computer Science (pp. 219-223). Springer International Publishing. doi:10.1007/978-3-030-17502-3_17
    Chapter. .
  • Malik, V., Hruska, M., Schrammel, P., & Vojnar, T. (2019). 2LS: Heap Analysis and Memory Safety (Competition Contribution). Retrieved from http://arxiv.org/abs/1903.00712v2
    Preprint.
  • Cordeiro, L. C., Kroening, D., & Schrammel, P. (2018). Benchmarking of Java verification tools at the software verification competition (SV-COMP). In Software Engineering Notes Vol. 43 (pp. 55-56). Florida, USA: Association for Computing Machinery. doi:10.1145/3282517.3282529
    Conference publication. .
  • Cordeiro, L., Kroening, D., & Schrammel, P. (2019). JBMC: Bounded Model Checking for Java Bytecode: (Competition Contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 11429 LNCS (pp. 219-223). doi:10.1007/978-3-030-17502-3_17
    Conference publication. .

2018

  • Malik, V., Hruska, M., Schrammel, P., & Vojnar, T. (2018, October 31). Template-based verification of heap-manipulating programs. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 鈥 November 2, 2018 (pp. 103-112). University of Texas, Austin, Texas: Institute of Electrical and Electronics Engineers.
    Conference publication. .
  • Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., & Trtik, M. (2018, July 14). JBMC: a bounded model checking tool for verifying java bytecode. In CAV 2018 Computer Aided Verification (pp. pages). Cham: Springer. doi:10.1007/978-3-319-96145-3_10
    Conference publication. .
  • Malik, V., Hruska, M., Schrammel, P., & Vojnar, T. (2018). Template-Based Verification of Heap-Manipulating Programs. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 (pp. 103-111). doi:10.23919/FMCAD.2018.8603009
    Conference publication. .
  • Mal铆k, V., Marti膷ek, 艩., Schrammel, P., Srivas, M., Vojnar, T., & Wahlang, J. (2018). 2LS: Memory Safety and Non-termination. In Lecture Notes in Computer Science (pp. 417-421). Springer International Publishing. doi:10.1007/978-3-319-89963-3_24
    Chapter. .
  • Malik, V., Marticek, 艩., Schrammel, P., Srivas, M., Vojnar, T., & Wahlang, J. (2018, April 14). 2LS: memory safety and non-termination (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Vol. 10806 (pp. 417-421). Thessaloniki, Greece: Springer. doi:10.1007/978-3-319-89963-3_24
    Conference publication. .

2017

  • Liang, L., Melham, T., Kroening, D., Schrammel, P., & Tautschnig, M. (2017). Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems, 17(2), 1-26. doi:10.1145/3147432
    Article. .
  • Chen, H. -Y., David, C., Kroening, D., Schrammel, P., & Wachter, B. (2017). Bit-precise procedure-modular termination analysis. ACM Transactions on Programming Languages and Systems, 40(1), 1-38. doi:10.1145/3121136
    Article. .
  • Nguyen, T. L., Schrammel, P., Fischer, B., Torre, S. L., & Parlato, G. (n.d.). Parallel bug-finding in concurrent programs via reduced interleaving instances. In Automated Software Engineering (pp. 753-764). University of Illinois: Association for Computing Machinery.
    Conference publication. .
  • Mukherjee, R., Schrammel, P., Haller, L., Kroening, D., & Melham, T. (2017). Lifting CDCL to template-based abstract domains for program verification. In Automated Technology for Verification and Analysis (pp. 307-326). Pune, India: Springer. doi:10.1007/978-3-319-68167-2_21
    Conference publication. .
  • Kumar, M., Schrammel, P., & Mandayam, S. (2017). Compositional safety refutation techniques. In Automated Technology for Verification and Analysis (pp. 164-183). Pune, India: Springer.
    Conference publication. .
  • Prabhu, S., Schrammel, P., Mandayam, S., Tautschnig, M., & Anand, Y. (2017, October 3). Concurrent program verification with invariant-guided underapproximation. In Automated Technology for Verification and Analysis (pp. 241-248). Pune, India: Springer. doi:10.1007/978-3-319-68167-2_17
    Conference publication. .
  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., & Bienm眉ller, T. (n.d.). Incremental bounded model checking for embedded software. Formal Aspects of Computing, 29(5), 911-931. doi:10.1007/s00165-017-0419-1
    Article. .
  • Cattaruzza, D., Abate, A., Schrammel, P., & Kroening, D. (2017). Sound numerical computations in abstract acceleration. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 10381 LNCS (pp. 38-60). doi:10.1007/978-3-319-63501-9_4
    Conference publication. .

2016

  • Kroening, D., Poetzl, D., Schrammel, P., & Wachter, B. (2016). Sound static deadlock analysis for C/Pthreads. In 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016) (pp. 379-390). New York, USA: ACM. doi:10.1145/2970276.2970309
    Chapter. .
  • Schrammel, P. (2016). Challenges in decomposing encodings of verification problems. Electronic Proceedings in Theoretical Computer Science, 219, 29-32. doi:10.4204/EPTCS.219.3
    Article. .
  • Nellis, A., Kesseli, P., Conmy, P. R., Kroening, D., Schrammel, P., & Tautschnig, M. (2016). Assisted coverage closure. In NASA formal methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, proceedings (Vol. 9690, pp. 49-64). Springer International Publishing. doi:10.1007/978-3-319-40648-0_5
    Chapter. .
  • Schrammel, P., & Kroening, D. (2016). 2LS for program analysis. In Tools and algorithms for the construction and analysis of systems (Vol. 9636, pp. 905-907). Berlin: Springer Berlin Heidelberg. doi:10.1007/978-3-662-49674-9_56
    Chapter. .
  • Mukherjee, R., Schrammel, P., Kroening, D., & Melham, T. (2016). Unbounded safety verification for hardware using software analyzers. In 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE) (pp. 1152-1155). Dresden, Germany: IEEE.
    Chapter. .
  • Chen, H. -Y., David, C., Kroening, D., Schrammel, P., & Wachter, B. (n.d.). Synthesising interprocedural bit-precise termination proofs. In Automated Software Engineering (ASE), 2015 30th IEEE/ACM International Conference on (pp. 53-64). IEEE. doi:10.1109/ASE.2015.10
    Chapter. .

2015

  • Schrammel, P. (n.d.). Unbounded-time reachability analysis of hybrid systems by abstract acceleration. In Proceedings of the 12th International Conference on Embedded Software (pp. 51-54). Piscataway, NJ: IEEE. doi:10.1109/EMSOFT.2015.7318259
    Chapter. .
  • Nellis, A., Kesseli, P., Conmy, P. R., Kroening, D., Schrammel, P., & Tautschnig, M. (2015). Assisted Coverage Closure. Retrieved from http://arxiv.org/abs/1509.04587v1
    Preprint.
  • Brain, M., Joshi, S., Kroening, D., & Schrammel, P. (2015). Safety verification and refutation by k-invariants and k-induction. In Unknown Book (Vol. 9291, pp. 145-161). Springer. doi:10.1007/978-3-662-48288-9_9
    Chapter. .
  • Cattaruzza, D., Abate, A., Schrammel, P., & Kroening, D. (2015). Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In Static analysis : 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings (pp. 312-331). Springer. doi:10.1007/978-3-662-48288-9_18
    Chapter. .
  • Brain, M., Joshi, S., Kroening, D., & Schrammel, P. (2015). Safety Verification and Refutation by k-invariants and k-induction (extended version). Retrieved from http://arxiv.org/abs/1506.05671v2
    Preprint.
  • Cattaruzza, D., Abate, A., Schrammel, P., & Kroening, D. (2015). Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version). Retrieved from http://arxiv.org/abs/1506.05607v5
    Preprint.
  • Chen, H. -Y., David, C., Kroening, D., Schrammel, P., & Wachter, B. (2015). Synthesising Interprocedural Bit-Precise Termination Proofs (extended version). Retrieved from http://arxiv.org/abs/1505.04581v1
    Preprint.
  • Kroening, D., Liang, L., Melham, T., Schrammel, P., & Tautschnig, M. (2015). Effective verification of low-level software with nested interrupts. In Proceedings -Design, Automation and Test in Europe, DATE Vol. 2015-April (pp. 229-234). doi:10.7873/date.2015.0360
    Conference publication. .
  • Kroening, D., Liang, L., Melham, T., Schrammel, P., & Tautschnig, M. (2015). Effective verification of low-level software with nested interrupts. In Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition (pp. 229-234). ACM.
    Chapter. .
  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., & Bienm眉ller, T. (2015). Successful use of incremental BMC in the automotive industry. In Formal methods for industrial critical systems : 20th International Workshop, FMICS 2015 Oslo, Norway, June 22-23, 2015 Proceedings (pp. 62-77). Springer. doi:10.1007/978-3-319-19458-5_5
    Chapter. .

2014

  • Schrammel, P., Melham, T., & Kroening, D. (2016). Generating test case chains for reactive systems. International Journal on Software Tools for Technology Transfer, 18(3), 319-334. doi:10.1007/s10009-014-0358-6
    Article. .
  • Gonnord, L., & Schrammel, P. (2014). Abstract acceleration in linear relation analysis. Science of Computer Programming, 93B, 125-153. doi:10.1016/j.scico.2013.09.016
    Article. .
  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., & Bienm眉ller, T. (2014). Incremental Bounded Model Checking for Embedded Software (extended version). Retrieved from http://arxiv.org/abs/1409.5872v1
    Preprint.
  • Monniaux, D., & Schrammel, P. (2014). Speeding Up Logico-Numerical Strategy Iteration (extended version). Retrieved from http://arxiv.org/abs/1403.2319v2
    Preprint.
  • Jeannet, B., Schrammel, P., & Sankaranarayanan, S. (2014). Abstract acceleration of general linear loops. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 529-540). doi:10.1145/2535838.2535843
    Conference publication. .
  • Seghir, M. N., & Schrammel, P. (2014). Necessary and sufficient preconditions via eager abstraction. In Programming languages and systems : 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings (pp. 236-254). Springer. doi:10.1007/978-3-319-12736-1_13
    Chapter. .
  • Rajan, A., Sharma, S., Schrammel, P., & Kroening, D. (2014). Accelerated test execution using GPUs. In ASE '14 Proceedings of the 29th ACM/IEEE international conference on Automated software engineering (pp. 97-102). New York, NY: ACM. doi:10.1145/2642937.2642957
    Chapter. .
  • Jeannet, B., Schrammel, P., & Sankaranarayanan, S. (2014). Abstract acceleration of general linear loops. In Unknown Book (Vol. 49, pp. 529-540). New York, NY, United States: ACM. doi:10.1145/2535838.2535843
    Chapter. .
  • Monniaux, D., & Schrammel, P. (2014). Speeding Up logico-numerical strategy iteration. In Static Analysis (Vol. 8723, pp. 253-267). Springer. doi:10.1007/978-3-319-10936-7_16
    Chapter. .

2013

  • Schrammel, P., Melham, T., & Kroening, D. (2013). Chaining Test Cases for Reactive System Testing (extended version). Retrieved from http://arxiv.org/abs/1306.3882v2
    Preprint.
  • Schrammel, P., & Subotic, P. (2013). Logico-numerical max-strategy iteration. In Verification, Model Checking, and Abstract Interpretation (Vol. 7737, pp. 414-433). Springer. doi:10.1007/978-3-642-35873-9_25
    Chapter. .
  • Schrammel, P., Melham, T., & Kroening, D. (2013). Chaining test cases for reactive dystem testing. In Testing Software and Systems (Vol. 8254, pp. 133-148). Springer. doi:10.1007/978-3-642-41707-8_9
    Chapter. .

2012

  • Schrammel, P., & Jeannet, B. (n.d.). Applying abstract acceleration to (co-)reachability analysis of reactive programs. Journal of Symbolic Computation, 47(12), 1512-1532. doi:10.1016/j.jsc.2011.12.051
    Article. .
  • Schrammel, P., & Jeannet, B. (2012). From hybrid data-flow languages to hybrid automata: A complete translation. In HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control (pp. 167-176). doi:10.1145/2185632.2185658
    Conference publication. .
  • Schrammel, P., & Jeannet, B. (2012). From hybrid data-flow languages to hybrid automata. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control - HSCC '12 (pp. 167-176). New York, NY: ACM. doi:10.1145/2185632.2185658
    Chapter. .

2011

  • Schrammel, P., & Jeannet, B. (2011). Logico-numerical abstract acceleration and application to the verification of data-flow programs. In Static Analysis (Vol. 6887, pp. 233-248). Springer. doi:10.1007/978-3-642-23702-7_19
    Chapter. .

2010

  • Schrammel, P., & Jeannet, B. (n.d.). Extending abstract acceleration methods to data-flow programs with numerical inputs. Electronic Notes in Theoretical Computer Science, 267(1), 101-114. doi:10.1016/j.entcs.2010.09.009
    Article. .

Unpublished works

  • Brain, M., David, C., Kroening, D., & Schrammel, P. (n.d.). Model and proof generation for heap-manipulating programs. In Programming languages and systems ESOP 2014 (Vol. 8410, pp. 432-452). Heidelberg: Springer. doi:10.1007/978-3-642-54833-8_23
    Chapter. .