Search results for "abstraction-refinement"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
17	Andreas Bauer 0002, Martin Leucker, Christian Schallhart, Michael Tautschnig	Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers.	ISoLA	2007	DBLP BibTeX RDF
17	Jörg Bauer 0001, Tobe Toben, Bernd Westphal	Mind the Shapes: Abstraction Refinement Via Topology Invariants.	ATVA	2007	DBLP DOI BibTeX RDF
17	Shengbing Jiang	Reachability Analysis Of Linear Hybrid Automata By Using Counterexample Fragment Based Abstraction Refinement.	ACC	2007	DBLP DOI BibTeX RDF
17	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	VCEGAR: Verilog CounterExample Guided Abstraction Refinement.	TACAS	2007	DBLP DOI BibTeX RDF
17	Stephanie Kemper, André Platzer	SAT-based Abstraction Refinement for Real-time Systems.	FACS	2006	DBLP DOI BibTeX RDF
17	Sumit Kumar Jha 0001	Numerical Simulation guided Lazy Abstraction Refinement for Nonlinear Hybrid Automata	CoRR	2006	DBLP BibTeX RDF
17	Freddy Y. C. Mang, Pei-Hsin Ho	Controllability and Cooperativeness Analysis for Automatic Abstraction Refinement.	Int. J. Found. Comput. Sci.	2006	DBLP DOI BibTeX RDF
17	Chao Wang 0001, Gary D. Hachtel, Fabio Somenzi	Abstraction Refinement for Large Scale Model Checking		2006	DOI RDF
17	Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar	Verifying analog oscillator circuits using forward/backward abstraction refinement.	DATE	2006	DBLP DOI BibTeX RDF
17	Jan-Willem Roorda	Semantics, Decision Procedures, and Abstraction Refinement for Symbolic Trajectory Evaluation.		2006	RDF
17	Annabelle McIver, Carroll Morgan	Abstraction, Refinement and Proof for Probabilistic Systems		2005	DOI RDF
17	Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic 0001	Abstraction-refinement for game-based model checking.	GALOP@ETAPS	2005	DBLP BibTeX RDF
17	Alexey Loginov, Thomas W. Reps, Shmuel Sagiv	Abstraction Refinement via Inductive Learning.	CAV	2005	DBLP DOI BibTeX RDF
17	Zhenyu Chen 0001, Conghua Zhou, Decheng Ding	Automatic abstraction refinement for Petri nets verification.	HLDVT	2005	DBLP DOI BibTeX RDF
17	Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic 0001	Data-Abstraction Refinement: A Game Semantic Approach.	SAS	2005	DBLP DOI BibTeX RDF
17	Bing Li, Chao Wang 0001, Fabio Somenzi	A satisfiability-based approach to abstraction refinement in model checking.	BMC@CAV	2003	DBLP DOI BibTeX RDF
17	Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke	Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.	SoftMC@CAV	2003	DBLP DOI BibTeX RDF
17	Dennis Dams	Comparing Abstraction Refinement Algorithms.	SoftMC@CAV	2003	DBLP DOI BibTeX RDF
17	Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald	Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement.	TACAS	2003	DBLP DOI BibTeX RDF
17	Edmund M. Clarke	Counterexample-Guided Abstraction Refinement.	TIME	2003	DBLP DOI BibTeX RDF
17	Andreas Podelski	Software Model Checking with Abstraction Refinement.	VMCAI	2003	DBLP DOI BibTeX RDF
17	Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang	Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis.	FMCAD	2002	DBLP DOI BibTeX RDF
17	Dong Wang, Pei-Hsin Ho, Jiang Long, James H. Kukula, Yunshan Zhu, Hi-Keung Tony Ma, Robert F. Damiano	Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines.	DAC	2001	DBLP DOI BibTeX RDF
17	Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu 0004, Helmut Veith	Counterexample-Guided Abstraction Refinement.	CAV	2000	DBLP DOI BibTeX RDF
17	Martin P. Ward	Abstraction refinement: A model of software evolution discussion by M. Ward.	J. Softw. Maintenance Res. Pract.	1995	DBLP DOI BibTeX RDF
17	Benjamin J. Keller, Richard E. Nance	Abstraction refinement: A model of software evolution.	J. Softw. Maintenance Res. Pract.	1993	DBLP DOI BibTeX RDF
17	Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani	Automatically Refining Abstract Interpretations.	TACAS	2008	DBLP DOI BibTeX RDF
17	Daniel Kroening, Natasha Sharygina	Approximating Predicate Images for Bit-Vector Logic.	TACAS	2006	DBLP DOI BibTeX RDF
17	Charles Lakos	Composing Abstractions of Coloured Petri Nets.	ICATPN	2000	DBLP DOI BibTeX RDF	Theory of High-Level Petri Nets, Refinement, Abstraction
16	Pritam Roy, David Parker 0001, Gethin Norman, Luca de Alfaro	Symbolic Magnifying Lens Abstraction in Markov Decision Processes.	QEST	2008	DBLP DOI BibTeX RDF
16	Barbara König 0001, Vitali Kozioura	Towards the Verification of Attributed Graph Transformation Systems.	ICGT	2008	DBLP DOI BibTeX RDF
16	Nannan He, Michael S. Hsiao	Bounded model checking of embedded software in wireless cognitive radio systems.	ICCD	2007	DBLP DOI BibTeX RDF
16	Edward Smith	A Logic for GSTE.	FMCAD	2007	DBLP DOI BibTeX RDF
16	Conghua Zhou	A compositional symbolic verification framework for concurrent software.	Infoscale	2007	DBLP DOI BibTeX RDF	model checking, composition, abstract, SAT
16	Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha 0001, Bruce H. Krogh	Refining Abstractions of Hybrid Systems Using Counterexample Fragments.	HSCC	2005	DBLP DOI BibTeX RDF
16	Arie Gurfinkel, Marsha Chechik	How Thorough Is Thorough Enough?	CHARME	2005	DBLP DOI BibTeX RDF
16	Alexander Asteroth, Christel Baier, Ulrich Aßmann	Model Checking with Formula-Dependent Abstract Models.	CAV	2001	DBLP DOI BibTeX RDF
15	Nikolaj S. Bjørner, Joe Hendrix	Linear Functional Fixed-points.	CAV	2009	DBLP DOI BibTeX RDF
15	Jonas Schrieb, Heike Wehrheim, Daniel Wonisch	Three-Valued Spotlight Abstractions.	FM	2009	DBLP DOI BibTeX RDF
15	Ansgar Fehnker, Ralf Huuck, Sean Seefried	Incremental False Path Elimination for Static Software Analysis.	ATVA	2009	DBLP DOI BibTeX RDF
15	Adam Bakewell, Dan R. Ghica	Compositional Predicate Abstraction from Game Semantics.	TACAS	2009	DBLP DOI BibTeX RDF
15	Kenneth L. McMillan, Lenore D. Zuck	Abstract Counterexamples for Non-disjunctive Abstractions.	RP	2009	DBLP DOI BibTeX RDF
15	Per Bjesse	Word-Level Sequential Memory Abstraction for Model Checking.	FMCAD	2008	DBLP DOI BibTeX RDF
15	Susmit Jha, Bryan A. Brady, Sanjit A. Seshia	Symbolic Reachability Analysis of Lazy Linear Hybrid Automata.	FORMATS	2007	DBLP DOI BibTeX RDF
15	Ferucio Laurentiu Tiplea, Constantin Enea	Abstractions of data types.	Acta Informatica	2006	DBLP DOI BibTeX RDF	Verification, Abstraction, Data type, Universal algebra
15	Harald Fecher, Martin Leucker, Verena Wolf	Don't Know in Probabilistic Systems.	SPIN	2006	DBLP DOI BibTeX RDF
15	Abelardo Pardo, Gary D. Hachtel	Automatic Abstraction Techniques for Propositional µ-calculus Model Checking.	CAV	1997	DBLP DOI BibTeX RDF
12	Matthias Heizmann, Jochen Hoenicke, Andreas Podelski	Refinement of Trace Abstraction.	SAS	2009	DBLP DOI BibTeX RDF
12	Bing Li, Fabio Somenzi	Efficient computation of small abstraction refinements.	ICCAD	2004	DBLP DOI BibTeX RDF
12	Mark Denford, Tim O'Neill, John Leaney	Architecture-Based Design of Computer Based Systems.	ECBS	2003	DBLP DOI BibTeX RDF
12	Sharon Barner, Daniel Geist, Anna Gringauze	Symbolic Localization Reduction with Reconstruction Layering and Backtracking.	CAV	2002	DBLP DOI BibTeX RDF
11	Marta Z. Kwiatkowska	On Quantitative Software Verification.	SPIN	2009	DBLP DOI BibTeX RDF
11	Marta Z. Kwiatkowska, Gethin Norman, David Parker 0001	Stochastic Games for Verification of Probabilistic Timed Automata.	FORMATS	2009	DBLP DOI BibTeX RDF
11	Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani	The MathSAT 4SMT Solver.	CAV	2008	DBLP DOI BibTeX RDF
11	Holger Hermanns, Björn Wachter, Lijun Zhang 0001	Probabilistic CEGAR.	CAV	2008	DBLP DOI BibTeX RDF
11	Goran Frehse, Sumit Kumar Jha 0001, Bruce H. Krogh	A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata.	HSCC	2008	DBLP DOI BibTeX RDF
11	Jörg Bauer 0001, Iovka Boneva, Marcos E. Kurbán, Arend Rensink	A Modal-Logic Based Graph Abstraction.	ICGT	2008	DBLP DOI BibTeX RDF
11	Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar	Proving Termination of Tree Manipulating Programs.	ATVA	2007	DBLP DOI BibTeX RDF
11	Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar	Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.	FMCAD	2007	DBLP DOI BibTeX RDF
11	Byron Cook, Andreas Podelski, Andrey Rybalchenko	Terminator: Beyond Safety.	CAV	2006	DBLP DOI BibTeX RDF
11	Dirk Beyer 0001, Thomas A. Henzinger, Grégory Théoduloz	Lazy Shape Analysis.	CAV	2006	DBLP DOI BibTeX RDF
11	Heike Wehrheim	Incremental Slicing.	ICFEM	2006	DBLP DOI BibTeX RDF
11	Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav	SATABS: SAT-Based Predicate Abstraction for ANSI-C.	TACAS	2005	DBLP DOI BibTeX RDF
11	Julien Allali, Marie-France Sagot	A Multiple Graph Layers Model with Application to RNA Secondary Structures Comparison.	SPIRE	2005	DBLP DOI BibTeX RDF	Graph layers, graph comparison, edit distance, secondary structure, RNA
11	Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith	Modular Verification of Software Components in C.	IEEE Trans. Software Eng.	2004	DBLP DOI BibTeX RDF
11	Alessandro Armando, Claudio Castellini, Jacopo Mantovani	Software Model Checking Using Linear Constraints.	ICFEM	2004	DBLP DOI BibTeX RDF
11	Edmund M. Clarke, Helmut Veith	Counterexamples Revisited: Principles, Algorithms, Applications.	Verification: Theory and Practice	2003	DBLP DOI BibTeX RDF
8	Dipankar Das 0002, P. P. Chakrabarti 0001, Rajeev Kumar 0004	Scenario-based timing verification of multiprocessor embedded applications.	ACM Trans. Design Autom. Electr. Syst.	2009	DBLP DOI BibTeX RDF	execution scenarios, real time systems, static timing analysis, Timing verification
8	Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva 0001, Karem A. Sakallah	A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas.	Constraints An Int. J.	2009	DBLP DOI BibTeX RDF	Infeasibility, Minimal unsatisfiable subformula, MUS, Smallest minimal unsatisfiable subformula, SMUS, SAT, Boolean satisfiability
8	Neha Rungta, Eric G. Mercer	Clash of the Titans: tools and techniques for hunting bugs in concurrent programs.	PADTAD	2009	DBLP DOI BibTeX RDF	testing and verification tools, evaluation, benchmarks, empirical study, concurrent programs
8	John W. O'Leary, Murali Talupur, Mark R. Tuttle	Protocol verification using flows: An industrial experience.	FMCAD	2009	DBLP DOI BibTeX RDF
8	Himanshu Jain, Edmund M. Clarke, Orna Grumberg	Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.	CAV	2008	DBLP DOI BibTeX RDF
8	David Lo 0001, Shahar Maoz	Hierarchical inter-object traces for specification mining.	OOPSLA Companion	2008	DBLP DOI BibTeX RDF	uml sequence diagram, live sequence charts, specification mining, object hierarchy
8	Kuntal Nanshi, Fabio Somenzi	Improved Visibility in One-to-Many Trace Concretization.	DATE	2008	DBLP DOI BibTeX RDF
8	Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening	Embedded software verification: challenges and solutions.	ICCAD	2008	DBLP DOI BibTeX RDF
8	Kenneth L. McMillan	Quantified Invariant Generation Using an Interpolating Saturation Prover.	TACAS	2008	DBLP DOI BibTeX RDF
8	Bernd Finkbeiner, Hans-Jörg Peter, Sven Schewe	RESY: Requirement Synthesis for Compositional Model Checking.	TACAS	2008	DBLP DOI BibTeX RDF
8	Kerstin Bauer, Raffaella Gentilini, Klaus Schneider 0001	A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata.	Haifa Verification Conference	2008	DBLP DOI BibTeX RDF
8	Li Li, Ming Gu 0001, Xiaoyu Song, Jianmin Wang 0001	Effective Predicate Abstraction for Program Verification.	TASE	2008	DBLP DOI BibTeX RDF	program verification, predicate abstraction
8	Ranjit Jhala, Kenneth L. McMillan	Array Abstractions from Proofs.	CAV	2007	DBLP DOI BibTeX RDF
8	Vijay Ganesh, David L. Dill	A Decision Procedure for Bit-Vectors and Arrays.	CAV	2007	DBLP DOI BibTeX RDF
8	Natasha Sharygina, Daniel Kröning	Model Checking with Abstraction for Web Services.	Test and Analysis of Web Services	2007	DBLP DOI BibTeX RDF
8	Federico Mari, Enrico Tronci	CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems.	HSCC	2007	DBLP DOI BibTeX RDF
8	Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang 0001, André Platzer, Marc Segelken, Boris Wirtz	Automating Verification of Cooperation, Control, and Design in Traffic Applications.	Formal Methods and Hybrid Real-Time Systems	2007	DBLP DOI BibTeX RDF
8	Sriram K. Rajamani	Static and Dynamic Analysis: Better Together.	APLAS	2007	DBLP DOI BibTeX RDF
8	Carsten Sinz	Compressing Propositional Proofs by Common Subproof Extraction.	EUROCAST	2007	DBLP DOI BibTeX RDF
8	Kelvin Ku, Thomas E. Hart, Marsha Chechik, David Lie	A buffer overflow benchmark for software model checkers.	ASE	2007	DBLP DOI BibTeX RDF	model checking, benchmark, buffer overflow, array bounds checking
8	Kenneth L. McMillan	Interpolants and Symbolic Model Checking.	VMCAI	2007	DBLP DOI BibTeX RDF
8	Arie Gurfinkel, Ou Wei, Marsha Chechik	Yasm: A Software Model-Checker for Verification and Refutation.	CAV	2006	DBLP DOI BibTeX RDF
8	Koushik Sen, Mahesh Viswanathan 0001	Model Checking Multithreaded Programs with Asynchronous Atomic Methods.	CAV	2006	DBLP DOI BibTeX RDF
8	Aleksandar S. Dimovski, Ranko Lazic 0001	Assume-Guarantee Software Verification Based on Game Semantics.	ICFEM	2006	DBLP DOI BibTeX RDF
8	Sharon Shoham, Orna Grumberg	3-Valued Abstraction: More Precision at Less Cost.	LICS	2006	DBLP DOI BibTeX RDF
8	Alexey Loginov, Thomas W. Reps, Mooly Sagiv	Refinement-Based Verification for Possibly-Cyclic Lists.	Program Analysis and Compilation	2006	DBLP DOI BibTeX RDF
8	Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili	Verifying Concurrent Message-Passing C Programs with Recursive Calls.	TACAS	2006	DBLP DOI BibTeX RDF
8	Byron Cook, Daniel Kroening, Natasha Sharygina	Over-Approximating Boolean Programs with Unbounded Thread Creation.	FMCAD	2006	DBLP DOI BibTeX RDF
8	Stefan Ratschan, Zhikun She	Constraints for Continuous Reachability in the Verification of Hybrid Systems.	AISC	2006	DBLP DOI BibTeX RDF
8	Gregorio Díaz 0001, Kim Guldstrand Larsen, Juan José Pardo, Fernando Cuartero, Valentín Valero	An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol.	SAC	2005	DBLP DOI BibTeX RDF	authentication protocols and model checking, system verification and model checking, security, e-commerce, authentication protocols
8	Arnaud Cuccuru, Robert de Simone, Thierry Saunier, Günther Siegel, Yves Sorel	P2I: An Innovative MDA Methodology for Embedded Real-Time System.	DSD	2005	DBLP DOI BibTeX RDF
8	Jochen Hoenicke, Patrick Maier 0001	Model-Checking of Specifications Integrating Processes, Data and Time.	FM	2005	DBLP DOI BibTeX RDF
8	Werner Damm, Guilherme Pinto, Stefan Ratschan	Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems.	ATVA	2005	DBLP DOI BibTeX RDF