Keyword:SMT

Publications
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint 13150
Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic Nikolaj Bjorner, Arie Gurfinkel, Sharon Shoham and Yakir Vizel EasyChair Preprint 10000
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
STLmc: Robust STL Model Checking of Hybrid Systems Using SMT Geunyeol Yu, Jia Lee and Kyungmin Bae EasyChair Preprint 8684
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5000
Extending VIAP to Handle Array Programs Pritom Rajkhowa and Fangzhen Lin EasyChair Preprint 393
Puli - A Problem-Specific OMT Solver Gergely Kovásznai, Csaba Biró and Balázs Erdélyi EasyChair Preprint 371
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint 1
Verifying SQL queries using theories of tables and relations Mudathir Mahgoub Yahia Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic Johannes Schoisswohl, Laura Kovács and Konstantin Korovin In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
On Symbolic Derivatives and Transition Regexes Margus Veanes In:LPAR 2024 Complementary Volume
Experiments on Infinite Model Finding in SMT Solving Julian Parsert, Chad Brown, Mikolas Janota and Cezary Kaliszyk In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Experimenting with Theory Instantiation in Vampire Martin Riener In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
On Inductive Verification and Synthesis Dennis Peuter and Viorica Sofronie-Stokkermans In:Selected Student Contributions and Workshop Papers of LuxLogAI 2018
Challenges for Fast Synthesis Procedures in SMT Andrew Reynolds In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Making Automatic Theorem Provers more Versatile Simon Cruanes In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Abduction for Learning Smart City Rules Nikolaj Bjorner, Maria-Cristina Marinescu and Mooly Sagiv In:GCAI 2017. 3rd Global Conference on Artificial Intelligence
SMT-Based CPS Parameter Synthesis Heinz Riener, Robert Koenighofer, Goerschwin Fey and Roderick Bloem In:ARCH16. 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems
Symbolic WS1S Loris D'Antoni and Margus Veanes In:LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations
Playing with Quantified Satisfaction Nikolaj Bjorner and Mikolas Janota In:LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations
SMT Encoding of Hybrid Systems in dReal Kyungmin Bae, Soonho Kong and Sicun Gao In:ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems
Instantiations, Zippers and EPR Interpolation Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Acceleration-based safety decision procedure for programs with arrays Francesco Alberti, Silvio Ghilardi and Natasha Sharygina In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
The 2012 SMT Competition David Cok, Alberto Griggio, Roberto Bruttomesso and Morgan Deters In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Program Verification as Satisfiability Modulo Theories Nikolaj Bjorner, Kenneth McMillan and Andrey Rybalchenko In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
SMT-LIB Sequences and Regular Expressions Nikolaj Bjorner, Vijay Ganesh, Raphaël Michel and Margus Veanes In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
An SMT-based approach to automated configuration Raphaël Michel, Arnaud Hubaux, Vijay Ganesh and Patrick Heymans In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width Gergely Kovásznai, Andreas Fröhlich and Armin Biere In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Anatomy of Alternating Quantifier Satisfiability (Work in progress) Anh-Dung Phan, Nikolaj Bjørner and David Monniaux In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems Mohammad Abdul Aziz, Amr Wassal and Nevine Darwish In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Reasoning with Triggers Claire Dross, Sylvain Conchon, Johannes Kanig and Andrei Paskevich In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed Iguernelala In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
SMT-Based System Verification with DVF Amit Goel, Sava Krstic, Rebekah Leslie and Mark Tuttle In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
A Theory of Arrays with set and copy Operations Stephan Falke, Carsten Sinz and Florian Merz In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Exploring Predictability of SAT/SMT Solvers Robert Brummayer, Duckki Oe and Aaron Stump In:EMSQMS 2010. Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions