| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Hana Chockler, Daniel Kroening, Mitra Purandare |
Computing Mutation Coverage in Interpolation-Based Model Checking.  |
IEEE Trans. on CAD of Integrated Circuits and Systems  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Vijay D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig |
Numeric Bounds Analysis with Conflict-Driven Learning. |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith |
Proving Reachability Using FShell - (Competition Contribution). |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl |
satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Georg Weissenbacher, Daniel Kroening, Sharad Malik |
Wolverine: Battling Bugs with Interpolants - (Competition Contribution). |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Tiziana Margaria, Jim Woodcock |
Editorial. |
Formal Asp. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl |
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report) |
CoRR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer |
Automatic analysis of DMA races using model checking and k-induction. |
Formal Methods in System Design |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening |
Loop Summarization and Termination Analysis. |
TACAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig |
Making Software Verification Tools Really Work. |
ATVA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Nannan He, Philipp Rümmer, Daniel Kroening |
Test-case generation for embedded simulink via formal concept analysis. |
DAC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig |
Soundness of Data Flow Analyses for Weak Memory Models. |
APLAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Georg Weissenbacher |
Interpolation-Based Software Verification with Wolverine. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl |
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
Linear Completeness Thresholds for Bounded Model Checking. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Barner, Ian G. Harris, Daniel Kroening, Orna Raz (eds.) |
Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers |
Haifa Verification Conference |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer |
Software Verification Using k-Induction. |
SAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. |
VMCAI |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Leopold Haller, Daniel Kroening |
Strengthening Induction-Based Race Checking with Lightweight Static Analysis. |
VMCAI |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer |
SCRATCH: a tool for automatic analysis of dma races. |
PPOPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Georg Weissenbacher |
Verification and falsification of programs with loops using predicate abstraction. |
Formal Asp. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Blanc, Daniel Kroening |
Race analysis for systemc using model checking. |
ACM Trans. Design Autom. Electr. Syst. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report) |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Daniel Kroening, Tiziana Margaria |
Verified software: theories, tools and experiments. |
STTT |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
Context-aware counter abstraction. |
Formal Methods in System Design |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Igor Zinovik, Yury Chebiryak, Daniel Kroening |
Periodic orbits and equilibria in glass models for gene regulatory networks. |
IEEE Transactions on Information Theory |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. |
IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer |
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. |
TACAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger |
Ranking Function Synthesis for Bit-Vector Relations. |
TACAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao |
Boom: Taking Boolean Program Model Checking One Step Further. |
TACAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Jérôme Leroux, Philipp Rümmer |
Interpolating Quantifier-Free Presburger Arithmetic. |
LPAR (Yogyakarta) |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer |
Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction. |
FMCO |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Daniel Kroening, Mitra Purandare |
Coverage in interpolation-based model checking. |
DAC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
Dynamic Cutoff Detection in Parameterized Concurrent Programs. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
Termination Analysis with Compositional Transition Invariants. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Vijay D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher |
Interpolant Strength. |
VMCAI |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Ofer Strichman |
A framework for Satisfiability Modulo Theories. |
Formal Asp. Comput. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
An abstraction-based decision procedure for bit-vector arithmetic. |
STTT |
2009 |
DBLP DOI BibTeX RDF |
Decision-procedures, Bit-vector |
| 1 | Daniel Kroening |
Software Verification. |
Handbook of Satisfiability |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
Loopfrog: A Static Analyzer for ANSI-C Programs. |
ASE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Thomas Wahl |
Mixed abstractions for floating-point arithmetic. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller |
Finding Lean Induced Cycles in Binary Hypercubes. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher |
Mutation-Based Test Case Generation for Simulink Models. |
FMCO |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Blanc, Daniel Kroening |
Speeding Up Simulation of SystemC Using Model Checking. |
SBMF |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Vijay D'Silva, Daniel Kroening |
Fixed points for multi-cycle path detection. |
DATE |
2009 |
DBLP BibTeX RDF |
|
| 1 | Mitra Purandare, Thomas Wahl, Daniel Kroening |
Strengthening properties using abstraction refinement. |
DATE |
2009 |
DBLP BibTeX RDF |
|
| 1 | Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
Symbolic Counter Abstraction for Concurrent Software. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Georg Weissenbacher |
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions. |
Haifa Verification Conference |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Yury Chebiryak, Daniel Kroening |
Towards a Classification of Hamiltonian Cycles in the 6-Cube. |
JSAT |
2008 |
DBLP BibTeX RDF |
|
| 1 | Vijay D'Silva, Daniel Kroening, Georg Weissenbacher |
A Survey of Automated Techniques for Formal Software Verification. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Thomas Wahl |
Craig Interpolation for Quantifier-Free Presburger Arithmetic |
CoRR |
2008 |
DBLP BibTeX RDF |
|
| 1 | Igor Zinovik, Daniel Kroening, Yury Chebiryak |
Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers. |
IEEE Transactions on Information Theory |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Blanc, Daniel Kroening, Natasha Sharygina |
Scoot: A Tool for the Analysis of SystemC Models. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
Loop Summarization Using Abstract Transformers. |
ATVA |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Vijay D'Silva, Mitra Purandare, Daniel Kroening |
Approximation Refinement for Interpolation-Based Model Checking. |
VMCAI |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening |
Embedded software verification: challenges and solutions. |
ICCAD |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Blanc, Daniel Kroening |
Race analysis for SystemC using model checking. |
ICCAD |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Verification of Boolean programs with unbounded thread creation. |
Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Himanshu Jain, Daniel Kroening |
Verification of SpecC using predicate abstraction. |
Formal Methods in System Design |
2007 |
DBLP DOI BibTeX RDF |
Verification, System level design, Predicate abstraction |
| 1 | Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
Deciding Bit-Vector Arithmetic with Abstraction. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
VCEGAR: Verilog CounterExample Guided Abstraction Refinement. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher |
Model checking concurrent linux device drivers. |
ASE |
2007 |
DBLP DOI BibTeX RDF |
model checking, linux, device driver, predicate abstraction |
| 1 | Nicolas Blanc, Alex Groce, Daniel Kroening |
Verifying C++ with STL containers via predicate abstraction. |
ASE |
2007 |
DBLP DOI BibTeX RDF |
model checking, verification, C++, iterator, predicate abstraction, STL |
| 1 | Daniel Kroening, Georg Weissenbacher |
Lifting Propositional Interpolants to the Word-Level. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Basler, Daniel Kroening, Georg Weissenbacher |
SAT-Based Summarization for Boolean Programs. |
SPIN |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Natasha Sharygina |
Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. |
DATE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Basler, Daniel Kroening, Georg Weissenbacher |
A Complete Bounded Model Checking Algorithm for Pushdown Systems. |
Haifa Verification Conference |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Sanjit A. Seshia |
Formal verification at higher levels of abstraction. |
ICCAD |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Igor Zinovik, Daniel Kroening, Yury Chebiryak |
An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors. |
AB |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger |
A First Step Towards a Unified Proof Checker for QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Natasha Sharygina, Daniel Kröning |
Model Checking with Abstraction for Web Services. |
Test and Analysis of Web Services |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening |
Computing Over-Approximations with Bounded Model Checking. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman |
Error explanation with distance metrics. |
STTT |
2006 |
DBLP DOI BibTeX RDF |
Error explanation, Model checking, Fault localization, Automated debugging |
| 1 | Daniel Kroening, Natasha Sharygina |
Approximating Predicate Images for Bit-Vector Logic. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Over-Approximating Boolean Programs with Unbounded Thread Creation. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Georg Weissenbacher |
Counterexamples with Loops for Predicate Abstraction. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz |
ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. |
Haifa Verification Conference |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Sven Beyer, Christian Jacobi 0002, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul |
Putting it all together - Formal verification of the VAMP. |
STTT |
2006 |
DBLP DOI BibTeX RDF |
Complete microprocessor verification, Tomasulo scheduler, Cache memory interface, Model checking, Formal methods, Theorem proving, Floating point unit |
| 1 | Alex Groce, Daniel Kroening |
Making the Most of BMC Counterexamples. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman |
Computational challenges in bounded model checking. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
Bonded-Model-checking, Completeness-Threshold, Complexity |
| 1 | Daniel Kroening, Natasha Sharygina |
Formal verification of SystemC by automatic hardware/software partitioning. |
MEMOCODE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
SATABS: SAT-Based Predicate Abstraction for ANSI-C. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Symbolic Model Checking for Asynchronous Boolean Programs. |
SPIN |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening |
Decision Procedures for the Grand Challenge. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Cogent: Accurate Theorem Proving for Program Verification. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
Predicate Abstraction of ANSI-C Programs Using SAT. |
Formal Methods in System Design |
2004 |
DBLP DOI BibTeX RDF |
ANSI-C, SAT, predicate abstraction |
| 1 | Daniel Kroening, Alex Groce, Edmund M. Clarke |
Counterexample Guided Abstraction Refinement Via Program Execution. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening |
Tutorial: Software Model Checking. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Himanshu Jain, Daniel Kroening, Edmund M. Clarke |
Verification of SpecC using predicate abstraction. |
MEMOCODE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Flavio Lerda |
A Tool for Checking ANSI-C Programs. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Jennifer Morris, Daniel Kroening, Philip Koopman |
Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems. |
DSN |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening |
A SAT-based algorithm for reparameterization in symbolic simulation. |
DAC |
2004 |
DBLP DOI BibTeX RDF |
SAT checkers, safety property checking, bounded model checking, symbolic simulation, parametric representation |
| 1 | Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman |
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Groce, Daniel Kroening, Flavio Lerda |
Understanding Counterexamples with explain. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Accurate Theorem Proving for Program Verification. |
ISoLA |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman |
Completeness and Complexity of Bounded Model Checking. |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Edmund M. Clarke |
Checking consistency of C and Verilog using predicate abstraction and induction. |
ICCAD |
2004 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")