The spirit of ghost codeFilliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei · Formal Methods in System Design · 2016

Let’s verify this with Why3Bobot, François; Filliâtre, Jean-Christophe; Marché, Claude; Paskevich, Andrei · International Journal on Software Tools for Technology Transfer · 2015

Adding Decision Procedures to SMT Solvers Using Axioms with TriggersDross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei · Journal of Automated Reasoning · 2016

[Lecture Notes in Computer Science] Verified Software. Theories, Tools, and Experiments Volume 10712 ||Paskevich, Andrei; Wies, Thomas · 2017

[Lecture Notes in Computer Science] Verified Software. Theories, Tools, and Experiments Volume 10712 || An Abstraction Technique for Describing Concurrent Program BehaviourPaskevich, Andrei; Wies, Thomas · 2017

[Lecture Notes in Computer Science] Verified Software. Theories, Tools, and Experiments Volume 10712 || Automating the Verification of Floating-Point ProgramsPaskevich, Andrei; Wies, Thomas · 2017

[Lecture Notes in Computer Science] Verified Software. Theories, Tools, and Experiments Volume 10712 || How to Get an Efficient yet Verified Arbitrary-Precision Integer LibraryPaskevich, Andrei; Wies, Thomas · 2017