Keyword:program analysis

Publications
HoRStify: Sound Security Analysis of Smart Contracts Sebastian Holler, Sebastian Biewer and Clara Schneidewind EasyChair Preprint 10335
Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm Guillaume Davy, Eric Feron, Pierre-Loic Garoche and Didier Henrion In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Moving the Needle on Rigorous Floating-Point Precision Tuning Marek Baranowski, Ian Briggs, Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric and Alexey Solovyev In:Automated Formal Methods
Cauliflower: a Solver Generator for Context-Free Language Reachability Nicholas Hollingum and Bernhard Scholz In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
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
Reasoning About Loops Using Vampire Laura Kovács and Simon Robillard In:Proceedings of the 1st and 2nd Vampire Workshops
Using Vampire in Soundness Proofs of Type Systems Sylvia Grewe, Sebastian Erdweg and Mira Mezini In:Proceedings of the 1st and 2nd Vampire Workshops
On Unfolding for Programs Using Strings as a Data Type Andrei Nemytykh In:VPT 2014. Second International Workshop on Verification and Program Transformation
A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? Alexei Lisitsa and Andrei Nemytykh In:VPT 2014. Second 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
Utilizing Hoare Logic to Strengthen Testing for Error Detection in Programs Shaoying Liu In:Turing-100. The Alan Turing Centenary
LOOPUS - A Tool for Computing Loop Bounds for C Programs Moritz Sinn and Florian Zuleger In:WING 2010. Workshop on Invariant Generation 2010