Search results for "SMT solver"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
2	Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine	veriT: An Open, Trustable and Efficient SMT-Solver.	CADE	2009	DBLP DOI BibTeX RDF
2	Robert Brummayer, Armin Biere	Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.	TACAS	2009	DBLP DOI BibTeX RDF
2	Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia	Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic.	CAV	2009	DBLP DOI BibTeX RDF
2	Dongyoon Lee, Mahmoud Said, Satish Narayanasamy, Zijiang Yang, Cristiano Pereira	Offline symbolic analysis for multi-processor execution replay.	MICRO	2009	DBLP DOI BibTeX RDF	multi-processor replay, shared-memory dependencies, SMT solver
2	Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer	Unifying type checking and property checking for low-level code.	POPL	2009	DBLP DOI BibTeX RDF	assertion checking, low-level code, decision procedure, type checking, smt solver, property checking
2	Leonardo Mendonça de Moura, Nikolaj Bjørner	Z3: An Efficient SMT Solver.	TACAS	2008	DBLP DOI BibTeX RDF
2	Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio	The Barcelogic SMT Solver.	CAV	2008	DBLP DOI BibTeX RDF
2	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	Aditi Tagore, Diego Zaccai, Bruce W. Weide	Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study.	NASA Formal Methods	2012	DBLP DOI BibTeX RDF
1	K. Rustan M. Leino	Automating Induction with an SMT Solver.	VMCAI	2012	DBLP DOI BibTeX RDF
1	Lina Bentakouk, Pascal Poizat, Fatiha Zaïdi	Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver.	TAP	2011	DBLP DOI BibTeX RDF
1	Bahareh Badban, Martin Lange	Exact Incremental Analysis of Timed Automata with an SMT-Solver.	FORMATS	2011	DBLP DOI BibTeX RDF
1	Evgeny Pavlenko, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Alexander Dreyer, Frank Seelisch, Gert-Martin Greuel	STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra.	DATE	2011	DBLP BibTeX RDF
1	Stefan J. Galler, Thomas Quaritsch, Martin Weiglhofer, Franz Wotawa	The IntiSa Approach: Test Input Data Generation for Non-primitive Data Types by Means of SMT Solver Based Bounded Model Checking.	QSIC	2011	DBLP DOI BibTeX RDF
1	Francis Palma, Angelo Susi, Paolo Tonella	Using an SMT solver for interactive requirements prioritization.	SIGSOFT FSE	2011	DBLP DOI BibTeX RDF
1	Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy	Semantic subtyping with an SMT solver.	ICFP	2010	DBLP DOI BibTeX RDF
1	Juan Chen, Ravi Chugh, Nikhil Swamy	Type-preserving compilation of end-to-end verification of security enforcement.	PLDI	2010	DBLP DOI BibTeX RDF	bytecode languages, compilers, authorization, functional programming, information flow, dependent types, security type systems, mobile code security
1	Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman	Continuity analysis of programs.	POPL	2010	DBLP DOI BibTeX RDF	stability, robustness, uncertainty, program analysis, continuity, errors, sensitivity, perturbations, proof rules
1	Matko Botincan, Matthew J. Parkinson, Wolfram Schulte	Separation Logic Verification of C Programs with an SMT Solver.	Electr. Notes Theor. Comput. Sci.	2009	DBLP DOI BibTeX RDF
1	Ganna Monakova, Oliver Kopp, Frank Leymann, Simon Moser, Klaus Schäfers	Verifying Business Rules Using an SMT Solver for BPEL Processes.	BPSC	2009	DBLP BibTeX RDF
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	Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala	Type-based data structure verification.	PLDI	2009	DBLP DOI BibTeX RDF	hindley-milner, type inference, dependent types, predicate abstraction
1	K. Rustan M. Leino, Rosemary Monahan	Reasoning about comprehensions with first-order SMT solvers.	SAC	2009	DBLP DOI BibTeX RDF	Spec#, matching triggers, quantifiers, SMT solvers
1	Jason Belt, Robby, Xianghua Deng	Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses.	ESEC/SIGSOFT FSE	2009	DBLP DOI BibTeX RDF	program analysis, symbolic execution, decision procedure
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Generalized, efficient array decision procedures.	FMCAD	2009	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Interpolant Generation for UTVPI.	CADE	2009	DBLP DOI BibTeX RDF
1	Nikolaj Bjørner, Joe Hendrix	Linear Functional Fixed-points.	CAV	2009	DBLP DOI BibTeX RDF
1	Vineet Kahlon, Chao Wang, Aarti Gupta	Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique.	CAV	2009	DBLP DOI BibTeX RDF
1	K. Rustan M. Leino, Ronald Middelkoop	Proving Consistency of Pure Methods and Model Fields.	FASE	2009	DBLP DOI BibTeX RDF
1	Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta	Symbolic Predictive Analysis for Concurrent Programs.	FM	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	Zijiang Yang, Bashar Al-Rawi, Karem A. Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu	Dynamic Path Reduction for Software Model Checking.	IFM	2009	DBLP DOI BibTeX RDF
1	Ilkka Niemelä	Integrating Answer Set Programming and Satisfiability Modulo Theories.	LPNMR	2009	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Nikolaj Bjørner	Satisfiability Modulo Theories: An Appetizer.	SBMF	2009	DBLP DOI BibTeX RDF
1	Andrea Calvagna, Angelo Gargantini	Combining Satisfiability Solving and Heuristics to Constrained Combinatorial Interaction Testing.	TAP	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	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	Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis	Refinement Types for Secure Implementations.	CSF	2008	DBLP DOI BibTeX RDF
1	Christopher Lynch, Duc-Khanh Tran	SMELS: Satisfiability Modulo Equality with Lazy Superposition.	ATVA	2008	DBLP DOI BibTeX RDF
1	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani	The MathSAT 4SMT Solver.	CAV	2008	DBLP DOI BibTeX RDF
1	A. K. McIver, Carroll C. Morgan, C. Gonzalia	Proofs and Refutations for Probabilistic Refinement.	FM	2008	DBLP DOI BibTeX RDF	quantitative program logic, refinement, constraint solving, counterexamples, Probabilistic systems
1	Ethan K. Jackson, Wolfram Schulte	Model Generation for Horn Logic with Stratified Negation.	FORTE	2008	DBLP DOI BibTeX RDF
1	Tommi A. Junttila, Jori Dubrovin	Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking.	LPAR	2008	DBLP DOI BibTeX RDF
1	Anindya Banerjee, Michael Barnett, David A. Naumann	Boogie Meets Regions: A Verification Experience Report.	VSTTE	2008	DBLP DOI BibTeX RDF
1	K. Rustan M. Leino	Specifying and verifying software.	ASE	2007	DBLP DOI BibTeX RDF	verification, specification, programming, automation, languages, tool support, SMT solver
1	Andreas Bauer 0002, Markus Pister, Michael Tautschnig	Tool-support for the analysis of hybrid systems and models.	DATE	2007	DBLP DOI BibTeX RDF
1	Shujun Deng, Jinian Bian, Weimin Wu, Xiaoqing Yang, Yanni Zhao	EHSAT: An Efficient RTL Satisfiability Solver Using an Extended DPLL Procedure.	DAC	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	Maria Paola Bonacina, Mnacho Echenim	T-Decision by Decomposition.	CADE	2007	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.	SAT	2007	DBLP DOI BibTeX RDF
1	Chao Wang, Aarti Gupta, Malay K. Ganai	Predicate learning and selective theory deduction for a difference logic solver.	DAC	2006	DBLP DOI BibTeX RDF	difference logic, SAT, decision procedure, SMT solver
1	Hossein M. Sheini, Karem A. Sakallah	A Progressive Simplifier for Satisfiability Modulo Theories.	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	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