Keyword:program verification

Publications
On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms Naoki Nishida, Misaki Kojima and Takumi Kato EasyChair Preprint 8673
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification Hrutvik Kanabar, Anthony Fox and Magnus O. Myreen EasyChair Preprint 8670
Verifying Numerical Programs via Iterative Abstract Testing Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang and Patrick Cousot EasyChair Preprint 1749
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart Wolff EasyChair Preprint 944
Program Analysis is Harder than Verification: A Computability Perspective Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato EasyChair Preprint 365
A FOOLish Encoding of the Next State Relations of Imperative Programs Evgenii Kotelnikov, Laura Kovács and Andrei Voronkov EasyChair Preprint 98
Automatic Bit- and Memory-Precise Verification of eBPF Code Martin Bromberger, Simon Schwarz and Christoph Weidenbach In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Automatic Detection of Vulnerable Variables for CTL Properties of Programs Naïm Moussaoui Remil, Caterina Urban and Antoine Miné In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Loop Analysis by Quantification over Iterations Bernhard Gleiss, Laura Kovács and Simon Robillard In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Reasoning about Translation Lookaside Buffers Hira Syeda and Gerwin Klein In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Proving uniformity and independence by self-composition and coupling Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu and Pierre-Yves Strub In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions Jon Hael Brenas, Rachid Echahed and Martin Strecker In:SCSS 2017. The 8th International Symposium on Symbolic Computation in Software Science 2017
Theory-Specific Reasoning about Loops with Arrays using Vampire Yuting Chen, Laura Kovacs and Simon Robillard In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
Verification of a brick Wang tiling algorithm Toshiaki Matsushima, Yoshihiro Mizoguchi and Alexandre Derouet-Jourdan In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Program Verification using Constraint Handling Rules and Array Constraint Generalizations Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti In:VPT 2014. Second International Workshop on Verification and Program Transformation
Program Verification as Satisfiability Modulo Theories Nikolaj Bjorner, Kenneth McMillan and Andrey Rybalchenko In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
HipSpec : Automating Inductive Proofs of Program Properties Koen Claessen, Moa Johansson, Dan Rosen and Nick Smallbone In:ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation
Verification of Imperative Programs through Transformation of Constraint Logic Programs Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti In:VPT 2013. First International Workshop on Verification and Program Transformation
Cryptographic Protocol Verification via Supercompilation (A Case Study) Abdulbasit Ahmed, Alexei Lisitsa and Andrei Nemytykh In:VPT 2013. First International Workshop on Verification and Program Transformation
Automated Invariant Generation for the Verification of Real-Time Systems Bahareh Badban, Stefan Leue and Jan-Georg Smaus In:WING 2010. Workshop on Invariant Generation 2010
Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper) Bernhard Beckert, Daniel Bruns and Sarah Grebing In:VERIFY-2010. 6th International Verification Workshop