Search results for "abstraction-refinement"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
75	Chao Wang 0001, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi	Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2006	DBLP DOI BibTeX RDF
66	Yan Chen 0001, Fei Xie, Jin Yang 0006	Optimizing automatic abstraction refinement for generalized symbolic trajectory evaluation.	DAC	2008	DBLP DOI BibTeX RDF	automatic abstraction refinement, generalized symbolic trajectory evaluation, model checking
65	Amir Pnueli	Using Abstraction to Verify Arbitrary Temporal Properties.	APSEC	2008	DBLP DOI BibTeX RDF
63	Byron Cook, Andreas Podelski, Andrey Rybalchenko	Abstraction Refinement for Termination.	SAS	2005	DBLP DOI BibTeX RDF
61	Francesco Ranzato, Olivia Rossi-Doria, Francesco Tapparo	A Forward-Backward Abstraction Refinement Algorithm.	VMCAI	2008	DBLP DOI BibTeX RDF
61	Chao Wang 0001, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi	Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement.	ICCAD	2003	DBLP DOI BibTeX RDF
60	Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav	Efficient Verification of Sequential and Concurrent C Programs.	Formal Methods Syst. Des.	2004	DBLP DOI BibTeX RDF	concurrency, process algebra, software verification, predicate abstraction, abstraction refinement
59	Amir Pnueli	Ranking Abstraction as a Companion to Predicate Abstraction, .	ATVA	2005	DBLP DOI BibTeX RDF
59	Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi	Property-Driven Partitioning for Abstraction Refinement.	TACAS	2007	DBLP DOI BibTeX RDF
59	Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich	The synergy of precise and fast abstractions for program verification.	SAC	2009	DBLP DOI BibTeX RDF	CEGAR, predicate abstraction, abstraction refinement
58	Bing Li, Chao Wang 0001, Fabio Somenzi	Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure.	Int. J. Softw. Tools Technol. Transf.	2005	DBLP DOI BibTeX RDF	Unsatisfiability proof, Bounded model checking, Satisfiability problem, Abstraction refinement
57	Constantin Enea	Counterexample Guided Abstraction Refinement is Better under Equational Abstraction.	ECBS	2008	DBLP DOI BibTeX RDF	equational abstraction, CEGAR, verification, refinement
56	Freddy Y. C. Mang, Pei-Hsin Ho	Abstraction refinement by controllability and cooperativeness analysis.	DAC	2004	DBLP DOI BibTeX RDF	formal verification, controllability, cooperativeness, abstraction refinement
56	Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi	Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation.	TACAS	2003	DBLP DOI BibTeX RDF
53	Yan Chen 0001, Yujing He, Fei Xie, Jin Yang 0006	Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation.	FMCAD	2007	DBLP DOI BibTeX RDF
51	Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith	State/Event Software Verification for Branching-Time Specifications.	IFM	2005	DBLP DOI BibTeX RDF	Concurrent Software Model Checking, State/Event-based Verification, Branching-time Temporal Logic, Automated Abstraction Refinement
51	Dirk Beyer 0001, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko	Path invariants.	PLDI	2007	DBLP DOI BibTeX RDF	invariant synthesis, formal verification, software model checking, predicate abstraction, abstraction refinement
50	Anubhav Gupta 0001, Ofer Strichman	Abstraction Refinement for Bounded Model Checking.	CAV	2005	DBLP DOI BibTeX RDF
49	Juncao Li, Xiuli Sun, Fei Xie, Xiaoyu Song	Component-Based Abstraction and Refinement.	ICSR	2008	DBLP DOI BibTeX RDF
49	Daniel Kroening, Alex Groce, Edmund M. Clarke	Counterexample Guided Abstraction Refinement Via Program Execution.	ICFEM	2004	DBLP DOI BibTeX RDF
48	Thomas Ball, Orna Kupferman	An Abstraction-Refinement Framework for Multi-Agent Systems.	LICS	2006	DBLP DOI BibTeX RDF
47	Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani	Abstraction Refinement of Linear Programs with Arrays.	TACAS	2007	DBLP DOI BibTeX RDF
46	Harald Fecher, Sharon Shoham	Local Abstraction-Refinement for the mu-Calculus.	SPIN	2007	DBLP DOI BibTeX RDF
46	Alexander Heußner, Tristan Le Gall, Grégoire Sutre	Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems.	SPIN	2009	DBLP DOI BibTeX RDF
45	Kuntal Nanshi, Fabio Somenzi	Constraints in one-to-many concretization for abstraction refinement.	DAC	2009	DBLP DOI BibTeX RDF	simulation, model checking, abstraction refinement
45	Manoranjan Satpathy, S. Ramesh 0002	Test case generation from formal models through abstraction refinement and model checking.	A-MOST	2007	DBLP DOI BibTeX RDF	counterexample guided abstraction refinement, model based testing, B-method
45	Bing Li, Fabio Somenzi	Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking.	TACAS	2006	DBLP DOI BibTeX RDF
44	Chao Wang 0001, Gary D. Hachtel, Fabio Somenzi	Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking.	ICCD	2004	DBLP DOI BibTeX RDF
44	Henning Dierks, Sebastian Kupferschmid, Kim Guldstrand Larsen	Automatic Abstraction Refinement for Timed Automata.	FORMATS	2007	DBLP DOI BibTeX RDF
44	Pei-Hsin Ho	Abstraction Refinement.	ATVA	2004	DBLP DOI BibTeX RDF
44	Jan-Georg Smaus, Jörg Hoffmann 0001	Relaxation Refinement: A New Method to Generate Heuristic Functions.	MoChArt	2008	DBLP DOI BibTeX RDF	Directed model checking, timed automata, predicate abstraction, abstraction refinement
42	Liang Zhang 0012, Mukul R. Prasad, Michael S. Hsiao, Thomas Sidle	Dynamic abstraction using SAT-based BMC.	DAC	2005	DBLP DOI BibTeX RDF	model checking, SAT, abstraction refinement
42	Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai	Localization and Register Sharing for Predicate Abstraction.	TACAS	2005	DBLP DOI BibTeX RDF
40	Nina Amla, Kenneth L. McMillan	Combining Abstraction Refinement and SAT-Based Model Checking.	TACAS	2007	DBLP DOI BibTeX RDF
40	Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah	Reveal: A Formal Verification Tool for Verilog Designs.	LPAR	2008	DBLP DOI BibTeX RDF
40	Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang 0001	Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop.	CAV	2006	DBLP DOI BibTeX RDF
39	Luca de Alfaro, Pritam Roy	Solving Games Via Three-Valued Abstraction Refinement.	CONCUR	2007	DBLP DOI BibTeX RDF
39	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina	Automated, compositional and iterative deadlock detection.	MEMOCODE	2004	DBLP DOI BibTeX RDF
38	Sharon Shoham, Orna Grumberg	A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.	CAV	2003	DBLP DOI BibTeX RDF
38	Maria Sorea	Lazy Approximation for Dense Real-Time Systems.	FORMATS/FTRTFT	2004	DBLP DOI BibTeX RDF
37	Sharon Shoham, Orna Grumberg	A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	3-valued semantics, Model checking games, Temporal logic, CTL, Counterexamples, Abstraction-Refinement
37	Andreas Podelski, Andrey Rybalchenko	ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement.	PADL	2007	DBLP DOI BibTeX RDF
37	Felix Klaedtke, Stefan Ratschan, Zhikun She	Language-Based Abstraction Refinement for Hybrid System Verification.	VMCAI	2007	DBLP DOI BibTeX RDF
37	Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang	Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.	CAV	2004	DBLP DOI BibTeX RDF
36	Edmund M. Clarke, Anubhav Gupta 0001, Ofer Strichman	SAT-based counterexample-guided abstraction refinement.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2004	DBLP DOI BibTeX RDF
36	Edmund M. Clarke, Anubhav Gupta 0001, James H. Kukula, Ofer Strichman	SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.	CAV	2002	DBLP DOI BibTeX RDF
36	Edmund M. Clarke	SAT-Based Counterexample Guided Abstraction Refinement.	SPIN	2002	DBLP DOI BibTeX RDF
36	Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic 0001	A Counterexample-Guided Refinement Tool for Open Procedural Programs.	SPIN	2006	DBLP DOI BibTeX RDF	CSP, software model checking, game semantics, abstraction refinement, FDR
36	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha 0001	Concurrent software verification with states, events, and deadlocks.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	Concurrent software, States and events, Counterexample-guided abstraction refinement, Model checking, Temporal logic, Deadlock, Compositional reasoning
35	Takeshi Nagaoka, Kozo Okano, Shinji Kusumoto	An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop.	IEICE Trans. Inf. Syst.	2010	DBLP DOI BibTeX RDF
34	Chao Wang 0001, Hyondeuk Kim, Aarti Gupta	Hybrid CEGAR: combining variable hiding and predicate abstraction.	ICCAD	2007	DBLP DOI BibTeX RDF
34	Thomas Ball, Andreas Podelski, Sriram K. Rajamani	Relative Completeness of Abstraction Refinement for Software Model Checking.	TACAS	2002	DBLP DOI BibTeX RDF
33	Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker 0001	Abstraction Refinement for Probabilistic Software.	VMCAI	2009	DBLP DOI BibTeX RDF
33	Tobe Toben	Counterexample Guided Spotlight Abstraction Refinement.	FORTE	2008	DBLP DOI BibTeX RDF
33	Stefan Ratschan, Zhikun She	Safety verification of hybrid systems by constraint propagation-based abstraction refinement.	ACM Trans. Embed. Comput. Syst.	2007	DBLP DOI BibTeX RDF	Hybrid systems, constraint propagation, intervals
33	Barbara König 0001, Vitali Kozioura	Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems.	TACAS	2006	DBLP DOI BibTeX RDF
33	Stefan Ratschan, Zhikun She	Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement.	HSCC	2005	DBLP DOI BibTeX RDF
33	Sharon Shoham, Orna Grumberg	Monotonic Abstraction-Refinement for CTL.	TACAS	2004	DBLP DOI BibTeX RDF
33	Sumit Kumar Jha 0001, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke	Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction.	HSCC	2007	DBLP DOI BibTeX RDF
33	Mar Yah Said, Michael J. Butler, Colin F. Snook	Language and Tool Support for Class and State Machine Refinement in UML-B.	FM	2009	DBLP DOI BibTeX RDF	UML, Formal specification, Refinement, Event-B, Visual modelling languages
32	Per Bjesse, James H. Kukula	Using Counter Example Guided Abstraction Refinement to Find Complex Bugs.	DATE	2004	DBLP DOI BibTeX RDF
32	Neha Rungta, Eric Mercer	Slicing and dicing bugs in concurrent programs.	ICSE (2)	2010	DBLP DOI BibTeX RDF	underapproximation, concurrency, abstraction-refinement
30	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2008	DBLP DOI BibTeX RDF
30	Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, Heike Wehrheim	Slicing Abstractions.	FSEN	2007	DBLP DOI BibTeX RDF
30	Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou	Automated Assume-Guarantee Reasoning by Abstraction Refinement.	CAV	2008	DBLP DOI BibTeX RDF
30	Javier Esparza, Stefan Kiefer, Stefan Schwoon	Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems.	TACAS	2006	DBLP DOI BibTeX RDF
30	Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer	Thread-Modular Abstraction Refinement.	CAV	2003	DBLP DOI BibTeX RDF
29	Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu 0004, Helmut Veith	Counterexample-guided abstraction refinement for symbolic model checking.	J. ACM	2003	DBLP DOI BibTeX RDF	temporal logic, Abstraction, symbolic model checking, hardware verification
28	Mohamed Nassim Seghir, Andreas Podelski	ACSAR: Software Model Checking with Transfinite Refinement.	SPIN	2007	DBLP DOI BibTeX RDF
28	Marc Segelken	Abstraction and Counterexample-Guided Construction of omega -Automata for Model Checking of Step-Discrete Linear Hybrid Models.	CAV	2007	DBLP DOI BibTeX RDF	automata construction, counterexample guidance, iterative abstraction refinement, step-discrete hybrid systems, model-checking
28	Kuntal Nanshi, Fabio Somenzi	Guiding simulation with increasingly refined abstract traces.	DAC	2006	DBLP DOI BibTeX RDF	simulation, model checking, abstraction refinement
27	Dennis Dams, Orna Grumberg	Abstraction and Abstraction Refinement.	Handbook of Model Checking	2018	DBLP DOI BibTeX RDF
27	Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer 0001, Bernd Becker 0001, Holger Hermanns	MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata.	QAPL	2014	DBLP DOI BibTeX RDF
27	Vitaly Kozyura	Abstraction and abstraction refinement in the verification of graph transformation systems. (PDF / PS)		2009	RDF
27	Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang	SAT Based Predicate Abstraction for Hardware Verification.	SAT	2003	DBLP DOI BibTeX RDF
25	Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies	Abstraction Refinement for Quantified Array Assertions.	SAS	2009	DBLP DOI BibTeX RDF
25	Fei He 0001, Xiaoyu Song, Ming Gu 0001, Jiaguang Sun 0001	Effective heuristics for counterexample-guided abstraction refinement.	ACM Great Lakes Symposium on VLSI	2007	DBLP DOI BibTeX RDF	model checking, verification, heuristics, SoC, abstraction
25	Jan-Willem Roorda, Koen Claessen	SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation.	CAV	2006	DBLP DOI BibTeX RDF
25	Fei He 0001, Xiaoyu Song, Ming Gu 0001, Jia-Guang Sun 0001	A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement.	ATVA	2006	DBLP DOI BibTeX RDF
25	Edmund M. Clarke	SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.	CADE	2003	DBLP DOI BibTeX RDF
25	Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah	Refinement strategies for verification methods based on datapath abstraction.	ASP-DAC	2006	DBLP DOI BibTeX RDF
25	Dinakar Dhurjati, Manuvir Das, Yue Yang	Path-Sensitive Dataflow Analysis with Iterative Refinement.	SAS	2006	DBLP DOI BibTeX RDF
25	Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar	Counterexample-Guided Control.	ICALP	2003	DBLP DOI BibTeX RDF
24	Vijay D'Silva, Sampada Sonalkar, S. Ramesh	Existential abstractions for distributed reactive systems via syntactic transformations.	EMSOFT	2007	DBLP DOI BibTeX RDF
24	Roman Gershman, Ofer Strichman	HaifaSat: A New Robust SAT Solver.	Haifa Verification Conference	2005	DBLP DOI BibTeX RDF
24	Abelardo Pardo, Gary D. Hachtel	Incremental CTL Model Checking Using BDD Subsetting.	DAC	1998	DBLP DOI BibTeX RDF	transceiver, spread spectrum communication, RF CMOS, digital radio, ISM frequency band
23	Kenneth L. McMillan	Toward Property-Driven Abstraction for Heap Manipulating Programs.	ATVA	2007	DBLP DOI BibTeX RDF
23	Roman Manevich, John Field, Thomas A. Henzinger, G. Ramalingam, Mooly Sagiv	Abstract Counterexample-Based Refinement for Powerset Domains.	Program Analysis and Compilation	2006	DBLP DOI BibTeX RDF
23	Fabio Somenzi	The Charme of Abstract Entities.	CHARME	2003	DBLP DOI BibTeX RDF
22	Martin T. Vechev, Eran Yahav, Greta Yorsh	Abstraction-guided synthesis of synchronization.	POPL	2010	DBLP DOI BibTeX RDF	concurrency, synthesis, abstract interpretation
22	Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke	Word level predicate abstraction and refinement for verifying RTL verilog.	DAC	2005	DBLP DOI BibTeX RDF	SAT, predicate abstraction, verilog
22	Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani	Refining Approximations in Software Predicate Abstraction.	TACAS	2004	DBLP DOI BibTeX RDF
20	Harald Fecher, Sharon Shoham	State Focusing: Lazy Abstraction for the Mu-Calculus.	SPIN	2008	DBLP DOI BibTeX RDF
20	Claudia Pons, Roxana S. Giandini, Gabriela Pérez, Pablo Pesce, Valeria Becker, Jorge Longinotti, Javier Cengia	PAMPERO: Precise Assistant for the Modeling Process in an Environment with Refinement Orientation.	UML Satellite Activities	2004	DBLP DOI BibTeX RDF
20	Ernst Moritz Hahn, Gethin Norman, David Parker 0001, Björn Wachter, Lijun Zhang 0001	Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems.	QEST	2011	DBLP DOI BibTeX RDF	probabilistic hybrid systems, probabilistic reachability, long-run average, abstraction refinement, stochastic games, controller synthesis
20	Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, SaiDeep Tetali, Aditya V. Thakur	Proofs from Tests.	IEEE Trans. Software Eng.	2010	DBLP DOI BibTeX RDF	Software model checking, abstraction refinement, directed testing
20	Matthias Heizmann, Jochen Hoenicke, Andreas Podelski	Nested interpolants.	POPL	2010	DBLP DOI BibTeX RDF	floyd-hoare logic, nested words, static analysis, interpolants, abstract interpretation, recursion, software model checking, abstraction refinement
20	Andreas Podelski, Thomas Wies	Counterexample-guided focus.	POPL	2010	DBLP DOI BibTeX RDF	quantified invariants, data structures, shape analysis, predicate abstraction, abstraction refinement
20	Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali	Compositional may-must program analysis: unleashing the power of alternation.	POPL	2010	DBLP DOI BibTeX RDF	software model checking, abstraction refinement, directed testing
20	Aditya V. Nori, Sriram K. Rajamani	An empirical study of optimizations in YOGI.	ICSE (1)	2010	DBLP DOI BibTeX RDF	testing, software model checking, abstraction refinement, directed testing