Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
77 | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
Counterexample-Guided Control. |
ICALP |
2003 |
DBLP DOI BibTeX RDF |
|
77 | 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 |
|
67 | Nina Amla, Kenneth L. McMillan |
A Hybrid of Counterexample-Based and Proof-Based Abstraction. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
61 | Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler |
Explaining Counterexamples Using Causality. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
57 | ShengYu Shen, Ying Qin, Sikun Li |
A Faster Counterexample Minimization Algorithm Based on Refutation Analysis. |
DATE |
2005 |
DBLP DOI BibTeX RDF |
|
57 | 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 |
|
57 | Edmund M. Clarke |
SAT-Based Counterexample Guided Abstraction Refinement. |
SPIN |
2002 |
DBLP DOI BibTeX RDF |
|
52 | Kazuhiro Ogata 0001, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi |
Induction-Guided Falsification. |
ICFEM |
2006 |
DBLP DOI BibTeX RDF |
observational transition system (OTS), invariant, induction, counterexample, Maude, CafeOBJ |
52 | Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster |
Scalable distributed on-the-fly symbolic model checking. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
Distributed, Memory, BDDs, Counterexample |
51 | 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 |
|
51 | Henning Dierks, Sebastian Kupferschmid, Kim Guldstrand Larsen |
Automatic Abstraction Refinement for Timed Automata. |
FORMATS |
2007 |
DBLP DOI BibTeX RDF |
|
51 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Abstraction Refinement for Termination. |
SAS |
2005 |
DBLP DOI BibTeX RDF |
|
51 | Paul Gastin, Pierre Moro, Marc Zeitoun |
Minimization of Counterexamples in SPIN. |
SPIN |
2004 |
DBLP DOI BibTeX RDF |
|
47 | Ralf Wimmer 0001, Bettina Braitling, Bernd Becker 0001 |
Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. |
VMCAI |
2009 |
DBLP DOI BibTeX RDF |
|
47 | 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 |
|
47 | Gabriel Mihai Lipsa, Nuno C. Martins |
Finite horizon optimal memoryless control of a delay in Gaussian noise: A simple counterexample. |
CDC |
2008 |
DBLP DOI BibTeX RDF |
|
47 | Junhua Zhang, Zhiqiu Huang, Zining Cao, Fangxiong Xiao |
Counterexample Generation for Probabilistic Timed Automata Model Checking. |
CSSE (2) |
2008 |
DBLP DOI BibTeX RDF |
|
47 | Marsha Chechik, Arie Gurfinkel |
A framework for counterexample generation and exploration. |
Int. J. Softw. Tools Technol. Transf. |
2007 |
DBLP DOI BibTeX RDF |
|
47 | Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita |
Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
47 | ShengYu Shen, Ying Qin, Sikun Li |
A fast counterexample minimization approach with refutation analysis and incremental SAT. |
ASP-DAC |
2005 |
DBLP DOI BibTeX RDF |
|
47 | ShengYu Shen, Ying Qin, Sikun Li |
Minimizing Counterexample with Unit Core Extraction and Incremental SAT. |
VMCAI |
2005 |
DBLP DOI BibTeX RDF |
|
47 | ShengYu Shen, Ying Qin, Sikun Li |
Localizing Errors in Counterexample with Iteratively Witness Searching. |
ATVA |
2004 |
DBLP DOI BibTeX RDF |
|
47 | 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 |
|
42 | Jinbiao Wang, Shu Qin |
The Research on Two Important Counter-Examples of Four-Color Problem. |
IITSI |
2010 |
DBLP DOI BibTeX RDF |
Tait conjecture, Kempe's chains, Heawood-counterexample, Tutte-counterexample, two-level Hamilton cycle |
41 | Mana Taghdiri, Daniel Jackson 0001 |
Inferring specifications to detect errors in code. |
Autom. Softw. Eng. |
2007 |
DBLP DOI BibTeX RDF |
Modular abstraction, Counterexample-guided abstraction refinement, Bounded program verification, SAT, Alloy, Specification inference |
41 | Dimiter Vakarelov |
Nelson's Negation on the Base of Weaker Versions of Intuitionistic Negation. |
Stud Logica |
2005 |
DBLP DOI BibTeX RDF |
Nelson negation, subminimal logic, counterexample semantics, many-valued logics |
41 | 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 |
41 | Tachio Terauchi |
Dependent types from counterexamples. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
interpolation, type inference, dependent types, counterexamples, intersection types |
41 | Matthias Schmalz, Daniele Varacca, Hagen Völzer |
Counterexamples in Probabilistic LTL Model Checking for Markov Chains. |
CONCUR |
2009 |
DBLP DOI BibTeX RDF |
|
41 | Ken-ichi Kawarabayashi, Bruce A. Reed |
Hadwiger's conjecture is decidable. |
STOC |
2009 |
DBLP DOI BibTeX RDF |
Hadwiger's conjecture, the four color theorem |
41 | Tsutomu Kumazawa, Tetsuo Tamai |
Iterative Model Fixing with Counterexamples. |
APSEC |
2008 |
DBLP DOI BibTeX RDF |
|
41 | Sanjay Jain 0001, Efim B. Kinber |
Learning Languages from Positive Data and Negative Counterexamples. |
ALT |
2004 |
DBLP DOI BibTeX RDF |
|
41 | Edmund M. Clarke, Helmut Veith |
Counterexamples Revisited: Principles, Algorithms, Applications. |
Verification: Theory and Practice |
2003 |
DBLP DOI BibTeX RDF |
|
41 | 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 |
|
41 | Dexter Kozen, Shmuel Zaks |
Optimal Bounds for the Change-Making Problem. |
ICALP |
1993 |
DBLP DOI BibTeX RDF |
|
38 | 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 |
37 | Tingting Han 0001, Joost-Pieter Katoen, Berteun Damman |
Counterexample Generation in Probabilistic Model Checking. |
IEEE Trans. Software Eng. |
2009 |
DBLP DOI BibTeX RDF |
|
37 | Constantin Enea |
Counterexample Guided Abstraction Refinement is Better under Equational Abstraction. |
ECBS |
2008 |
DBLP DOI BibTeX RDF |
equational abstraction, CEGAR, verification, refinement |
37 | Pulkit Grover, Anant Sahai |
A vector version of witsenhausen's counterexample: A convergence of control, communication and computation. |
CDC |
2008 |
DBLP DOI BibTeX RDF |
|
37 | Tamer Basar |
Variations on the theme of the Witsenhausen counterexample. |
CDC |
2008 |
DBLP DOI BibTeX RDF |
|
37 | 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 |
|
37 | Barbara König 0001, Vitali Kozioura |
Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
37 | ShengYu Shen, Ying Qin, Sikun Li |
Minimizing Counterexample of ACTL Property. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Toshiji Kawagoe, Shihomi Wada |
The Bullwhip Effect: A Counterexample. |
IAT |
2005 |
DBLP DOI BibTeX RDF |
Beer Game, Supply chain, multiagent simulation, bullwhip effect |
37 | Marsha Chechik, Arie Gurfinkel |
A Framework for Counterexample Generation and Exploration. |
FASE |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, Stefan Leue |
Heuristic-guided counterexample search in FLAVERS. |
SIGSOFT FSE |
2004 |
DBLP DOI BibTeX RDF |
FLAVERS, heuristic search, counterexamples |
37 | Edmund M. Clarke |
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
31 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker. |
APSEC |
2005 |
DBLP DOI BibTeX RDF |
lockout freedom property, mutual exclusion property, model checking, rewriting logic, counterexample |
31 | Ranjit Jhala, Rupak Majumdar |
Path slicing. |
PLDI |
2005 |
DBLP DOI BibTeX RDF |
counterexample analysis, program slicing |
31 | Gihwon Kwon |
Applying Model Checking Techniques to Game Solving. |
SERA |
2003 |
DBLP DOI BibTeX RDF |
game solving, Model checking, counterexample, state explosion problem |
31 | Tomoya Horiguchi, Tsukasa Hirashima |
The Role of Counterexamples in Discovery Learning Environment: Awareness of the Chance for Learning. |
JSAI Workshops |
2001 |
DBLP DOI BibTeX RDF |
discovery learning environment, simulation, education, counterexample, CAI |
30 | Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman |
Error explanation with distance metrics. |
Int. J. Softw. Tools Technol. Transf. |
2006 |
DBLP DOI BibTeX RDF |
Error explanation, Model checking, Fault localization, Automated debugging |
30 | Chao Wang 0001, Zijiang Yang 0006, Franjo Ivancic, Aarti Gupta |
Whodunit? Causal Analysis for Counterexamples. |
ATVA |
2006 |
DBLP DOI BibTeX RDF |
|
30 | Orna Kupferman, Sarai Sheinvald-Faragy |
Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words. |
CONCUR |
2006 |
DBLP DOI BibTeX RDF |
|
30 | Sriram K. Rajamani |
Automatic Property Checking for Software: Past, Present and Future. |
ASE |
2006 |
DBLP DOI BibTeX RDF |
|
30 | Kavita Ravi, Fabio Somenzi |
Minimal Assignments for Bounded Model Checking. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
30 | Alex Groce |
Error Explanation with Distance Metrics. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
30 | Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang |
SAT Based Predicate Abstraction for Hardware Verification. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
30 | Jean-Marie Le Bars |
The 0-1 law fails for frame satisfiability of propositional modal logic. |
LICS |
2002 |
DBLP DOI BibTeX RDF |
Computational Complexity, Finite Model Theory, Modal and Temporal Logics |
30 | Desh Ranjan, Suresh Chari, Pankaj Rohatgi |
Improving Known Solutions is Hard. |
ICALP |
1991 |
DBLP DOI BibTeX RDF |
|
27 | Philippe Langevin, Gregor Leander, Gary McGuire |
A Counterexample to a Conjecture of Niho. |
IEEE Trans. Inf. Theory |
2007 |
DBLP DOI BibTeX RDF |
|
27 | Paul Gastin, Pierre Moro |
Minimal Counterexample Generation for SPIN. |
SPIN |
2007 |
DBLP DOI BibTeX RDF |
|
27 | 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 |
27 | Y.-H. Kim |
A Counterexample to Cover's 2P Conjecture on Gaussian Feedback Capacity. |
IEEE Trans. Inf. Theory |
2006 |
DBLP DOI BibTeX RDF |
|
27 | 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 |
|
27 | Bhargav S. Gulavani, Sriram K. Rajamani |
Counterexample Driven Refinement for Abstract Interpretation. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
27 | Haibin Kan, Hong Shen 0001 |
A counterexample for the open problem on the minimal delays of orthogonal designs with maximal rates. |
IEEE Trans. Inf. Theory |
2005 |
DBLP DOI BibTeX RDF |
|
27 | 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 |
|
27 | Toshiji Kawagoe, Shihomi Wada |
A Counterexample for the Bullwhip Effect: Gaming and Multiagent Simulations. |
JSAI Workshops |
2005 |
DBLP DOI BibTeX RDF |
Beer Game, Supply chain, multiagent simulation, bullwhip effect |
27 | Daniel Kroening, Alex Groce, Edmund M. Clarke |
Counterexample Guided Abstraction Refinement Via Program Execution. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Robert Meolic, Alessandro Fantechi, Stefania Gnesi |
Witness and Counterexample Automata for ACTL. |
FORTE |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Pranava K. Jha |
A Counterexample to Tang and Padubidri's Claim about the Bisection Width of a Diagonal Mesh. |
IEEE Trans. Computers |
2003 |
DBLP DOI BibTeX RDF |
Diagonal mesh, bisection width |
27 | Daniel Jackson 0001, Craig Damon |
Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. |
IEEE Trans. Software Eng. |
1996 |
DBLP DOI BibTeX RDF |
model checking, formal specification, software design, Z notation, Abstract modeling, exhaustive testing |
27 | Daniel Jackson 0001, Craig Damon |
Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. |
ISSTA |
1996 |
DBLP DOI BibTeX RDF |
|
21 | Muhammad-Naeem Irfan |
State Machine Inference in Testing Context with Long Counterexamples. |
ICST |
2010 |
DBLP DOI BibTeX RDF |
state machine inference, finite state machine, black box, counterexample |
21 | Liping Li, Huaikou Miao, Shengbo Chen |
Test Generation for Web Applications Using Model-Checking. |
SNPD |
2010 |
DBLP DOI BibTeX RDF |
test deduction rule, model checking, Web application, test cases, styling, counterexample |
21 | Ranjit Jhala, Rupak Majumdar |
Software model checking. |
ACM Comput. Surv. |
2009 |
DBLP DOI BibTeX RDF |
counterexample-guided refinement, enumerative and symbolic model checking, abstraction, safety, liveness, Software model checking |
21 | Tomoya Horiguchi, Tsukasa Hirashima |
Domain-Independent Error-Based Simulation for Error-Awareness and Its Preliminary Evaluation. |
PRICAI |
2008 |
DBLP DOI BibTeX RDF |
simulation-based learning environment, learner’s error, intelligent tutoring system, counterexample, truth maintenance system |
21 | 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 |
21 | James Cheney, Alberto Momigliano |
Mechanized metatheory model-checking. |
PPDP |
2007 |
DBLP DOI BibTeX RDF |
counterexample search, model checking, nominal logic |
21 | Westley Weimer |
Patches as better bug reports. |
GPCE |
2006 |
DBLP DOI BibTeX RDF |
localization, error, explanation, patch, bug, counterexample, bug report |
21 | Dana N. Xu |
Extended static checking for haskell. |
Haskell |
2006 |
DBLP DOI BibTeX RDF |
counterexample guided unrolling, pre/postcondition, symbolic simplification |
21 | Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar |
Joining dataflow with predicates. |
ESEC/SIGSOFT FSE |
2005 |
DBLP DOI BibTeX RDF |
counterexample analysis, model checking, dataflow analysis, predicate abstraction |
21 | Gordon J. Pace, Nicolas Halbwachs, Pascal Raymond |
Counter-example generation in symbolic abstract model-checking. |
Int. J. Softw. Tools Technol. Transf. |
2004 |
DBLP DOI BibTeX RDF |
Concrete counterexample, Model-checking, Abstraction, Test pattern generation |
21 | HoonSang Jin, Kavita Ravi, Fabio Somenzi |
Fate and free will in error traces. |
Int. J. Softw. Tools Technol. Transf. |
2004 |
DBLP DOI BibTeX RDF |
Reachability game, Model checking, Counterexample |
21 | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan |
Abstractions from proofs. |
POPL |
2004 |
DBLP DOI BibTeX RDF |
counterexample analysis, software model checking, predicate abstraction |
21 | Fady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi |
Efficient debugging in a formal verification environment. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
Counter-example, Model checking, Counterexample |
21 | Gordon D. Plotkin |
Three Inadequate Models. |
Formal Aspects Comput. |
2002 |
DBLP DOI BibTeX RDF |
Full abstraction, Counterexample, PCF, Adequacy |
20 | Tetsuo Hasegawa, Yoshiaki Fukazawa |
Model Checking by Generating Observers from an Interface Specification Between Components. |
UNISCON |
2009 |
DBLP DOI BibTeX RDF |
model cheking, UML, timing diagram |
20 | Joshua D. Guttman |
Cryptographic Protocol Composition via the Authentication Tests. |
FoSSaCS |
2009 |
DBLP DOI BibTeX RDF |
|
20 | Radu Iosif, Adam Rogalewicz |
Automata-Based Termination Proofs. |
CIAA |
2009 |
DBLP DOI BibTeX RDF |
|
20 | Kenneth L. McMillan, Lenore D. Zuck |
Abstract Counterexamples for Non-disjunctive Abstractions. |
RP |
2009 |
DBLP DOI BibTeX RDF |
|
20 | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah |
Reveal: A Formal Verification Tool for Verilog Designs. |
LPAR |
2008 |
DBLP DOI BibTeX RDF |
|
20 | Armando Solar-Lezama, Christopher Grant Jones, Rastislav Bodík |
Sketching concurrent data structures. |
PLDI |
2008 |
DBLP DOI BibTeX RDF |
concurrency, synthesis, sketching, sat, spin |
20 | Francesco Ranzato, Olivia Rossi-Doria, Francesco Tapparo |
A Forward-Backward Abstraction Refinement Algorithm. |
VMCAI |
2008 |
DBLP DOI BibTeX RDF |
|
20 | Barbara König 0001, Vitali Kozioura |
Towards the Verification of Attributed Graph Transformation Systems. |
ICGT |
2008 |
DBLP DOI BibTeX RDF |
|
20 | Duminda Wijesekera, Paul Ammann, Lingya Sun, Gordon Fraser 0001 |
Relating counterexamples to test cases in CTL model checking specifications. |
A-MOST |
2007 |
DBLP DOI BibTeX RDF |
test coverage criteria, model checking, formal methods, software testing, state machines, counterexamples |
20 | Ranjit Jhala, Kenneth L. McMillan |
Array Abstractions from Proofs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
20 | Marc Herbstritt, Vanessa Struve, Bernd Becker 0001 |
Application of Lifting in Partial Design Analysis. |
MTV |
2007 |
DBLP DOI BibTeX RDF |
|
20 | Tobias Nopper, Christoph Scholl 0001, Bernd Becker 0001 |
Computation of minimal counterexamples by using black box techniques and symbolic methods. |
ICCAD |
2007 |
DBLP DOI BibTeX RDF |
|