Search results for "unbounded model checking"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Magdalena Kacprzak, Wojciech Penczek	Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic1.	Autonomous Agents and Multi-Agent Systems	2005	DBLP DOI BibTeX RDF	Alternating-time Temporal Logic, unbounded model checking, SAT-based verification, multi-agent systems, symbolic model checking
3	Magdalena Kacprzak, Alessio Lomuscio, T. Lasica, Wojciech Penczek, Maciej Szreter	Verifying Multi-agent Systems via Unbounded Model Checking.	FAABS	2004	DBLP DOI BibTeX RDF	unbounded model checking, multi-agent systems, Model checking
2	Bing Li, Fabio Somenzi	Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking.	TACAS	2006	DBLP DOI BibTeX RDF
2	Florian Pigorsch, Christoph Scholl, Stefan Disch	Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling.	FMCAD	2006	DBLP DOI BibTeX RDF
2	Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer	Stepping forward with interpolants in unbounded model checking.	ICCAD	2006	DBLP DOI BibTeX RDF
2	Kameshwar Chandrasekar, Michael S. Hsiao	State Set Management for SAT-based Unbounded Model Checking.	ICCD	2005	DBLP DOI BibTeX RDF
2	Malay K. Ganai, Aarti Gupta, Pranav Ashar	Beyond safety: customized SAT-based model checking.	DAC	2005	DBLP DOI BibTeX RDF	circuit cofactoring, unbounded model checking, formal verification, SAT, liveness, bounded model checking, LTL
2	Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek	Verification of Multiagent Systems via Unbounded Model Checking.	AAMAS	2004	DBLP DOI BibTeX RDF
2	Magdalena Kacprzak, Wojciech Penczek	Unbounded Model Checking for Alternating-Time Temporal Logic.	AAMAS	2004	DBLP DOI BibTeX RDF
1	Hu-Hsi Yeh, Cheng-Yin Wu, Chung-Yang (Ric) Huang	Property-specific sequential invariant extraction for SAT-based unbounded model checking.	ICCAD	2011	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer	Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking.	IEEE Trans. on CAD of Integrated Circuits and Systems	2010	DBLP DOI BibTeX RDF
1	Takafumi Matsuo, Tatsuhiro Tsuchiya, Tohru Kikuno	Feature Interaction Verification Using Unbounded Model Checking with Interpolation.	IEICE Transactions	2009	DBLP BibTeX RDF
1	Yakir Vizel, Orna Grumberg	Interpolation-sequence based model checking.	FMCAD	2009	DBLP DOI BibTeX RDF
1	Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah	A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas.	Constraints	2009	DBLP DOI BibTeX RDF	Infeasibility, Minimal unsatisfiable subformula, MUS, Smallest minimal unsatisfiable subformula, SMUS, SAT, Boolean satisfiability
1	Wojciech Penczek, Maciej Szreter	SAT-based Unbounded Model Checking of Timed Automata.	Fundam. Inform.	2008	DBLP BibTeX RDF
1	Gianpiero Cabodi, Paolo Camurati, Luz Garcia, Marco Murciano, Sergio Nocco, Stefano Quer	Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking.	FMCAD	2008	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Paolo Camurati, Marco Murciano	Automated abstraction by incremental refinement in interpolant-based model checking.	ICCAD	2008	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer	Boosting interpolation with dynamic localized abstraction and redundancy removal.	ACM Trans. Design Autom. Electr. Syst.	2008	DBLP DOI BibTeX RDF	Interpolant, abstraction, redundancy removal
1	Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige	Challenges in Constraint-Based Analysis of Hybrid Systems.	CSCLP	2008	DBLP DOI BibTeX RDF	mixed Boolean and arithmetic constraints, stochastic SMT, parallel solver, differential equations, Craig interpolation
1	Wojciech Penczek, Maciej Szreter	SAT-based Unbounded Model Checking of Timed Automata.	ACSD	2007	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Sergio Nocco, Stefano Quer	Boosting the role of inductive invariants in model checking.	DATE	2007	DBLP DOI BibTeX RDF
1	Arie Matsliah, Ofer Strichman	Underapproximation for Model-Checking Based on Random Cryptographic Constructions.	CAV	2007	DBLP DOI BibTeX RDF
1	Nina Amla, Kenneth L. McMillan	Combining Abstraction Refinement and SAT-Based Model Checking.	TACAS	2007	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Marco Crivellari, Sergio Nocco, Stefano Quer	Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking.	DATE	2005	DBLP DOI BibTeX RDF
1	Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip	Symmetry Reduction in SAT-Based Model Checking.	CAV	2005	DBLP DOI BibTeX RDF
1	Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan	An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment.	CHARME	2005	DBLP DOI BibTeX RDF
1	João P. Marques Silva	Improvements to the Implementation of Interpolant-Based Model Checking.	CHARME	2005	DBLP DOI BibTeX RDF
1	Malay K. Ganai, Aarti Gupta, Pranav Ashar	DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems.	TACAS	2005	DBLP DOI BibTeX RDF
1	HoonSang Jin, HyoJung Han, Fabio Somenzi	Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit.	TACAS	2005	DBLP DOI BibTeX RDF
1	Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek	From Bounded to Unbounded Model Checking for Temporal Epistemic Logic.	Fundam. Inform.	2004	DBLP BibTeX RDF
1	Fang Yu, Bow-Yaw Wang	Toward Unbounded Model Checking for Region Automata.	ATVA	2004	DBLP DOI BibTeX RDF	Region automata, Real-time systems, Model checking, Verification, Induction, BMC
1	Shuo Sheng, Michael S. Hsiao	Success-Driven Learning in ATPG for Preimage Computation.	IEEE Design & Test of Computers	2004	DBLP DOI BibTeX RDF
1	Wojciech Penczek, Agata Pólrola	Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata.	ICATPN	2004	DBLP DOI BibTeX RDF
1	Kenneth L. McMillan	Methods for exploiting SAT solvers in unbounded model checking.	MEMOCODE	2003	DBLP DOI BibTeX RDF
1	Kenneth L. McMillan, Nina Amla	Automatic Abstraction without Counterexamples.	TACAS	2003	DBLP DOI BibTeX RDF
1	Gianpiero Cabodi, Sergio Nocco, Stefano Quer	Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification.	CAV	2002	DBLP DOI BibTeX RDF