Search results for "satisfiability modulo theories"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump	Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Competition, Decision procedures, Automated theorem proving, SMT, Satisfiability modulo theories
3	Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump	Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005).	J. Autom. Reasoning	2005	DBLP DOI BibTeX RDF	competition, decision procedures, satisfiability modulo theories
2	Hyondeuk Kim, Fabio Somenzi, HoonSang Jin	Efficient Term-ITE Conversion for Satisfiability Modulo Theories.	SAT	2009	DBLP DOI BibTeX RDF
2	Leonardo Mendonça de Moura, Nikolaj Bjørner	Satisfiability Modulo Theories: An Appetizer.	SBMF	2009	DBLP DOI BibTeX RDF
2	Ilkka Niemelä	Integrating Answer Set Programming and Satisfiability Modulo Theories.	LPNMR	2009	DBLP DOI BibTeX RDF
2	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Efficient Interpolant Generation in Satisfiability Modulo Theories.	TACAS	2008	DBLP DOI BibTeX RDF
2	Tommi A. Junttila, Jori Dubrovin	Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking.	LPAR	2008	DBLP DOI BibTeX RDF
2	Tino Teige, Martin Fränzle	Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic.	CPAIOR	2008	DBLP DOI BibTeX RDF
2	Margus Veanes, Ando Saabas	Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract).	ABZ	2008	DBLP DOI BibTeX RDF
2	Yeting Ge, Clark Barrett, Cesare Tinelli	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.	CADE	2007	DBLP DOI BibTeX RDF
2	Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio	Challenges in Satisfiability Modulo Theories.	RTA	2007	DBLP DOI BibTeX RDF
2	Cesare Tinelli	An Abstract Framework for Satisfiability Modulo Theories.	TABLEAUX	2007	DBLP DOI BibTeX RDF
2	Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar	A Tutorial on Satisfiability Modulo Theories.	CAV	2007	DBLP DOI BibTeX RDF
2	Hossein M. Sheini, Karem A. Sakallah	A Progressive Simplifier for Satisfiability Modulo Theories.	SAT	2006	DBLP DOI BibTeX RDF
2	Hossein M. Sheini, Karem A. Sakallah	From Propositional Satisfiability to Satisfiability Modulo Theories.	SAT	2006	DBLP DOI BibTeX RDF
2	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani	Efficient Satisfiability Modulo Theories via Delayed Theory Combination.	CAV	2005	DBLP DOI BibTeX RDF
2	Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump	SMT-COMP: Satisfiability Modulo Theories Competition.	CAV	2005	DBLP DOI BibTeX RDF
1	Mnacho Echenim, Nicolas Peltier	An Instantiation Scheme for Satisfiability Modulo Theories.	J. Autom. Reasoning	2012	DBLP DOI BibTeX RDF
1	Jianmin Zhang, ShengYu Shen, Jun Zhang, Weixia Xu, Sikun Li	Extracting minimal unsatisfiable subformulas in satisfiability modulo theories.	Comput. Sci. Inf. Syst.	2011	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Satisfiability modulo theories: introduction and applications.	Commun. ACM	2011	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.	J. Artif. Intell. Res. (JAIR)	2011	DBLP BibTeX RDF
1	Carlos Ansótegui, Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret	Satisfiability Modulo Theories: An Efficient Approach for the Resource-Constrained Project Scheduling Problem.	SARA	2011	DBLP BibTeX RDF
1	Philippe Suter, Robin Steiger, Viktor Kuncak	Sets with Cardinality Constraints in Satisfiability Modulo Theories.	VMCAI	2011	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Efficient generation of craig interpolants in satisfiability modulo theories.	ACM Trans. Comput. Log.	2010	DBLP DOI BibTeX RDF
1	Cesare Tinelli	Foundations of Satisfiability Modulo Theories.	WoLLIC	2010	DBLP DOI BibTeX RDF
1	Felix Reimann, Michael Glaß, Christian Haubelt, Michael Eberl, Jürgen Teich	Improving platform-based system synthesis by satisfiability modulo theories solving.	CODES+ISSS	2010	DBLP DOI BibTeX RDF
1	Maria Paola Bonacina	On theorem proving for program checking: historical perspective and recent developments.	PPDP	2010	DBLP DOI BibTeX RDF	combination of theories, rewrite-based theorem proving, speculative inferences, satisfiability modulo theories
1	Lucas Cordeiro, Bernd Fischer 0002, João Marques-Silva	Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking.	ECBS	2010	DBLP DOI BibTeX RDF	Embedded Software Verification, Bounded Model Checking, Satisfiability Modulo Theories
1	Margus Veanes, Peli de Halleux, Nikolai Tillmann	Rex: Symbolic Regular Expression Explorer.	ICST	2010	DBLP DOI BibTeX RDF	regular expressions, finite automata, strings, satisfiability modulo theories
1	Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari	Oracle-guided component-based program synthesis.	ICSE	2010	DBLP DOI BibTeX RDF	oracle-based learning, SAT, program synthesis, SMT
1	Daniel Kroening, Ofer Strichman	A framework for Satisfiability Modulo Theories.	Formal Asp. Comput.	2009	DBLP DOI BibTeX RDF
1	Aaron Stump	Proof Checking Technology for Satisfiability Modulo Theories.	Electr. Notes Theor. Comput. Sci.	2009	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories	CoRR	2009	DBLP BibTeX RDF
1	Yeting Ge, Clark W. Barrett, Cesare Tinelli	Solving quantified verification conditions using satisfiability modulo theories.	Ann. Math. Artif. Intell.	2009	DBLP DOI BibTeX RDF
1	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani	Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.	Ann. Math. Artif. Intell.	2009	DBLP DOI BibTeX RDF
1	Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli	Satisfiability Modulo Theories.	Handbook of Satisfiability	2009	DBLP DOI BibTeX RDF
1	Thomas Heinz, Reinhard Wilhelm	Towards device emulation code generation.	LCTES	2009	DBLP DOI BibTeX RDF	bit vector arithmetic, device emulation, code generation, binary translation, satisfiability modulo theories
1	Lucas Cordeiro, Bernd Fischer 0002, João Marques-Silva	SMT-Based Bounded Model Checking for Embedded ANSI-C Software.	ASE	2009	DBLP DOI BibTeX RDF	Embedded ANSI-C Software, Bounded Model Checking, Satisfiability Modulo Theories
1	Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary	Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions.	PEPM	2009	DBLP DOI BibTeX RDF	static array bounds checking, verilog elaboration, verilog wire width consistency, dependent types, dead code elimination
1	Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura	On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving.	CADE	2009	DBLP DOI BibTeX RDF
1	Feifei Ma, Sheng Liu, Jian Zhang 0001	Volume Computation for Boolean Combination of Linear Arithmetic Constraints.	CADE	2009	DBLP DOI BibTeX RDF
1	Yeting Ge, Leonardo Mendonça de Moura	Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories.	CAV	2009	DBLP DOI BibTeX RDF
1	Nikolaj Bjørner, Leonardo Mendonça de Moura	Tapas: Theory Combinations and Practical Applications.	FORMATS	2009	DBLP DOI BibTeX RDF
1	Pascal Fontaine	Combinations of Theories for Decidable Fragments of First-Order Logic.	FroCos	2009	DBLP DOI BibTeX RDF
1	Margus Veanes, Pavel Grigorenko, Peli de Halleux, Nikolai Tillmann	Symbolic Query Exploration.	ICFEM	2009	DBLP DOI BibTeX RDF
1	Tomi Janhunen, Ilkka Niemelä, Mark Sevalnev	Computing Stable Models via Reductions to Difference Logic.	LPNMR	2009	DBLP DOI BibTeX RDF
1	Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov	Path Feasibility Analysis for String-Manipulating Programs.	TACAS	2009	DBLP DOI BibTeX RDF
1	Robert Brummayer, Armin Biere	Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.	TACAS	2009	DBLP DOI BibTeX RDF
1	Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid	Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints.	TACAS	2009	DBLP DOI BibTeX RDF
1	Alessandro Armando, Jacopo Mantovani, Lorenzo Platania	Bounded model checking of software using SMT solvers instead of SAT solvers.	STTT	2009	DBLP DOI BibTeX RDF
1	Clark Barrett, Morgan Deters, Albert Oliveras, Aaron Stump	Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007).	International Journal on Artificial Intelligence Tools	2008	DBLP DOI BibTeX RDF
1	David Déharbe, Silvio Ranise, Jorgiano Vidal	A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework.	J. Braz. Comp. Soc.	2008	DBLP DOI BibTeX RDF
1	Shuvendu K. Lahiri, Shaz Qadeer	Back to the future: revisiting precise program verification using SMT solvers.	POPL	2008	DBLP DOI BibTeX RDF	heap-manipulating programs, software verification, decision procedures, reachability, linked lists, SMT solvers
1	Mingxuan Yuan, Xiuqiang He, Zonghua Gu	Hardware/Software Partitioning and Static Task Scheduling on Runtime Reconfigurable FPGAs using a SMT Solver.	IEEE Real-Time and Embedded Technology and Applications Symposium	2008	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Towards SMT Model Checking of Array-Based Systems.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Engineering DPLL(T) + Saturation.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Margus Veanes, Nikolaj Bjørner, Alexander Raschke	An SMT Approach to Bounded Reachability Analysis of Model Programs.	FORTE	2008	DBLP DOI BibTeX RDF
1	Margus Veanes, Ando Saabas	On Bounded Reachability of Programs with Set Comprehensions.	LPAR	2008	DBLP DOI BibTeX RDF
1	Saswat Anand, Patrice Godefroid, Nikolai Tillmann	Demand-Driven Compositional Symbolic Execution.	TACAS	2008	DBLP DOI BibTeX RDF
1	Michal Moskal	Rocket-Fast Proof Checking for SMT Solvers.	TACAS	2008	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Z3: An Efficient SMT Solver.	TACAS	2008	DBLP DOI BibTeX RDF
1	Ilkka Niemelä	Stable models and difference logic.	Ann. Math. Artif. Intell.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68N17, 68T27
1	Cesare Tinelli	Trends and Challenges in Satisfiability Modulo Theories.	VERIFY	2007	DBLP BibTeX RDF
1	Daniel Kroening, Sanjit A. Seshia	Formal verification at higher levels of abstraction.	ICCAD	2007	DBLP DOI BibTeX RDF
1	Lee Pike	Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules.	FMCAD	2007	DBLP DOI BibTeX RDF
1	Geoffrey M. Brown, Lee Pike	Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols.	MEMOCODE	2007	DBLP DOI BibTeX RDF
1	Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti	Verifying Heap-Manipulating Programs in an SMT Framework.	ATVA	2007	DBLP DOI BibTeX RDF
1	David Walter, Scott Little, Chris J. Myers	Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver.	ATVA	2007	DBLP DOI BibTeX RDF
1	Maria Paola Bonacina, Mnacho Echenim	T-Decision by Decomposition.	CADE	2007	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.	CADE	2007	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Efficient E-Matching for SMT Solvers.	CADE	2007	DBLP DOI BibTeX RDF
1	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani	A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.	CAV	2007	DBLP DOI BibTeX RDF
1	Olga Ohrimenko, Peter J. Stuckey, Michael Codish	Propagation = Lazy Clause Generation.	CP	2007	DBLP DOI BibTeX RDF
1	Roberto Sebastiani	From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain.	FroCos	2007	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Decision procedures for extensions of the theory of arrays.	Ann. Math. Artif. Intell.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68T27, 03B25, 03B70, 68T15
1	Anders Franzén	Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs.	Electr. Notes Theor. Comput. Sci.	2006	DBLP DOI BibTeX RDF
1	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani	Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis.	LPAR	2006	DBLP DOI BibTeX RDF
1	Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T).	J. ACM	2006	DBLP DOI BibTeX RDF	SAT solvers, Satisfiability Modulo Theories
1	Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani	Intelligent Systems and Formal Methods in Software Engineering.	IEEE Intelligent Systems	2006	DBLP DOI BibTeX RDF	deductive software verification, software engineering, formal methods, program verification, software synthesis, satisfiability modulo theories
1	Hossein M. Sheini, Karem A. Sakallah	SMT(CLU): a step toward scalability in system verification.	ICCAD	2006	DBLP DOI BibTeX RDF
1	Hossein M. Sheini, Karem A. Sakallah	Ario: A Linear Integer Arithmetic Logic Solver.	FMCAD	2006	DBLP DOI BibTeX RDF
1	Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Splitting on Demand in SAT Modulo Theories.	LPAR	2006	DBLP DOI BibTeX RDF
1	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani	To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT).	LPAR	2006	DBLP DOI BibTeX RDF
1	Yinlei Yu, Sharad Malik	Lemma Learning in SMT on Linear Constraints.	SAT	2006	DBLP DOI BibTeX RDF
1	Alessandro Armando, Jacopo Mantovani, Lorenzo Platania	Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers.	SPIN	2006	DBLP DOI BibTeX RDF
1	Geoffrey M. Brown, Lee Pike	Easy Parameterized Verification of Biphase Mark and 8N1 Protocols.	TACAS	2006	DBLP DOI BibTeX RDF
1	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
1	Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Massimo Idini, Marco Maratea	TSAT++: an Open Platform for Satisfiability Modulo Theories.	Electr. Notes Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
1	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani	The MathSAT 3 System.	CADE	2005	DBLP DOI BibTeX RDF
1	Robert Nieuwenhuis, Albert Oliveras	DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic.	CAV	2005	DBLP DOI BibTeX RDF
1	Natarajan Shankar	Inference Systems for Logical Algorithms.	FSTTCS	2005	DBLP DOI BibTeX RDF
1	Filip Maric, Predrag Janicic	argo-lib: A Generic Platform for Decision Procedures.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Cesare Tinelli	A DPLL-Based Calculus for Ground Satisfiability Modulo Theories.	JELIA	2002	DBLP DOI BibTeX RDF