Keyword:SMT

Papers
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint no. 13150
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
Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic Nikolaj Bjorner, Arie Gurfinkel, Sharon Shoham and Yakir Vizel EasyChair Preprint no. 10000
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 9606
STLmc: Robust STL Model Checking of Hybrid Systems Using SMT Geunyeol Yu, Jia Lee and Kyungmin Bae EasyChair Preprint no. 8684
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 5000
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
Extending VIAP to Handle Array Programs Pritom Rajkhowa and Fangzhen Lin EasyChair Preprint no. 393
Puli - A Problem-Specific OMT Solver Gergely Kovásznai, Csaba Biró and Balázs Erdélyi EasyChair Preprint no. 371
Making Automatic Theorem Provers more Versatile Simon Cruanes In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Challenges for Fast Synthesis Procedures in SMT Andrew Reynolds 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
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint no. 1
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
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
Symbolic WS1S Loris D'Antoni and Margus Veanes 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
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
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
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
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
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed Iguernlala 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
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems Mohammad Abdul Aziz, Amr Wassal and Nevin Darwish In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Anatomy of Alternating Quantifier Satisfiability (Work in progress) Anh-Dung Phan, Nikolaj Bjorner and David Monniaux 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
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
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
Program Verification as Satisfiability Modulo Theories Nikolaj Bjorner, Kenneth L. McMillan and Andrey Rybalchenko In:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
The 2012 SMT Competition David Cok, Alberto Griggio, Roberto Bruttomesso and Morgan Deters 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