|
Search the dblp DataBase
Daniel Kroening:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
Publications of Author
- Silvia M. Müller, Holger W. Leister, Peter Dell, Nikolaus Gerteis, Daniel Kroening
The Impact of Hardware Scheduling Mechanismus on the Performance and Cost of Processor Designs. [Citation Graph (0, 0)][DBLP] ARCS, 1999, pp:65-73 [Conf]
- Byron Cook, Daniel Kroening, Natasha Sharygina
Cogent: Accurate Theorem Proving for Program Verification. [Citation Graph (0, 0)][DBLP] CAV, 2005, pp:296-300 [Conf]
- Alex Groce, Daniel Kroening, Flavio Lerda
Understanding Counterexamples with explain. [Citation Graph (0, 0)][DBLP] CAV, 2004, pp:453-456 [Conf]
- Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. [Citation Graph (0, 0)][DBLP] CAV, 2004, pp:308-320 [Conf]
- Daniel Kroening, Georg Weissenbacher
Counterexamples with Loops for Predicate Abstraction. [Citation Graph (0, 0)][DBLP] CAV, 2006, pp:152-165 [Conf]
- Sven Beyer, Chris Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. [Citation Graph (0, 0)][DBLP] CHARME, 2003, pp:51-65 [Conf]
- Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening
A SAT-based algorithm for reparameterization in symbolic simulation. [Citation Graph (0, 0)][DBLP] DAC, 2004, pp:524-529 [Conf]
- Edmund M. Clarke, Daniel Kroening, Karen Yorav
Behavioral consistency of C and verilog programs using bounded model checking. [Citation Graph (0, 0)][DBLP] DAC, 2003, pp:368-371 [Conf]
- Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Word level predicate abstraction and refinement for verifying RTL verilog. [Citation Graph (0, 0)][DBLP] DAC, 2005, pp:445-450 [Conf]
- Daniel Kroening, Wolfgang J. Paul
Automated Pipeline Design. [Citation Graph (0, 0)][DBLP] DAC, 2001, pp:810-815 [Conf]
- Jennifer Morris, Daniel Kroening, Philip Koopman
Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded Systems. [Citation Graph (0, 0)][DBLP] DSN, 2004, pp:377-0 [Conf]
- Byron Cook, Daniel Kroening, Natasha Sharygina
Over-Approximating Boolean Programs with Unbounded Thread Creation. [Citation Graph (0, 0)][DBLP] FMCAD, 2006, pp:53-59 [Conf]
- Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz
ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. [Citation Graph (0, 0)][DBLP] Haifa Verification Conference, 2006, pp:138-154 [Conf]
- Daniel Kroening, Edmund M. Clarke
Checking consistency of C and Verilog using predicate abstraction and induction. [Citation Graph (0, 0)][DBLP] ICCAD, 2004, pp:66-72 [Conf]
- Edmund M. Clarke, Daniel Kroening, Karen Yorav
Specifying and Verifying Systems with Multiple Clocks. [Citation Graph (0, 0)][DBLP] ICCD, 2003, pp:48-0 [Conf]
- Edmund M. Clarke, Daniel Kroening
Tutorial: Software Model Checking. [Citation Graph (0, 0)][DBLP] ICFEM, 2004, pp:9-10 [Conf]
- Daniel Kroening, Alex Groce, Edmund M. Clarke
Counterexample Guided Abstraction Refinement Via Program Execution. [Citation Graph (0, 0)][DBLP] ICFEM, 2004, pp:224-238 [Conf]
- Byron Cook, Daniel Kroening, Natasha Sharygina
Accurate Theorem Proving for Program Verification. [Citation Graph (0, 0)][DBLP] ISoLA, 2004, pp:96-114 [Conf]
- Himanshu Jain, Daniel Kroening, Edmund M. Clarke
Verification of SpecC using predicate abstraction. [Citation Graph (0, 0)][DBLP] MEMOCODE, 2004, pp:7-16 [Conf]
- Daniel Kroening, Natasha Sharygina
Formal verification of SystemC by automatic hardware/software partitioning. [Citation Graph (0, 0)][DBLP] MEMOCODE, 2005, pp:101-110 [Conf]
- Byron Cook, Daniel Kroening, Natasha Sharygina
Symbolic Model Checking for Asynchronous Boolean Programs. [Citation Graph (0, 0)][DBLP] SPIN, 2005, pp:75-90 [Conf]
- Edmund M. Clarke, Daniel Kroening, Flavio Lerda
A Tool for Checking ANSI-C Programs. [Citation Graph (0, 0)][DBLP] TACAS, 2004, pp:168-176 [Conf]
- Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
SATABS: SAT-Based Predicate Abstraction for ANSI-C. [Citation Graph (0, 0)][DBLP] TACAS, 2005, pp:570-574 [Conf]
- Daniel Kroening, Natasha Sharygina
Approximating Predicate Images for Bit-Vector Logic. [Citation Graph (0, 0)][DBLP] TACAS, 2006, pp:242-256 [Conf]
- Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Completeness and Complexity of Bounded Model Checking. [Citation Graph (0, 0)][DBLP] VMCAI, 2004, pp:85-96 [Conf]
- Daniel Kroening, Ofer Strichman
Efficient Computation of Recurrence Diameters. [Citation Graph (0, 0)][DBLP] VMCAI, 2003, pp:298-309 [Conf]
- Alex Groce, Daniel Kroening
Making the Most of BMC Counterexamples. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2005, v:119, n:2, pp:67-81 [Journal]
- Daniel Kroening
Computing Over-Approximations with Bounded Model Checking. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:1, pp:79-92 [Journal]
- Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
Predicate Abstraction of ANSI-C Programs Using SAT. [Citation Graph (0, 0)][DBLP] Formal Methods in System Design, 2004, v:25, n:2-3, pp:105-127 [Journal]
- Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Computational challenges in bounded model checking. [Citation Graph (0, 0)][DBLP] STTT, 2005, v:7, n:2, pp:174-183 [Journal]
- Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman
Error explanation with distance metrics. [Citation Graph (0, 0)][DBLP] STTT, 2006, v:8, n:3, pp:229-247 [Journal]
- Daniel Kroening, Natasha Sharygina
Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. [Citation Graph (0, 0)][DBLP] DATE, 2007, pp:1325-1330 [Conf]
- Gérard Basler, Daniel Kroening, Georg Weissenbacher
SAT-Based Summarization for Boolean Programs. [Citation Graph (0, 0)][DBLP] SPIN, 2007, pp:131-148 [Conf]
- Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
VCEGAR: Verilog CounterExample Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP] TACAS, 2007, pp:583-586 [Conf]
- Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
Deciding Bit-Vector Arithmetic with Abstraction. [Citation Graph (0, 0)][DBLP] TACAS, 2007, pp:358-372 [Conf]
- Igor Zinovik, Daniel Kroening, Yury Chebiryak
An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors. [Citation Graph (0, 0)][DBLP] AB, 2007, pp:140-154 [Conf]
- Edmund M. Clarke, Himanshu Jain, Daniel Kroening
Verification of SpecC using predicate abstraction. [Citation Graph (0, 0)][DBLP] Formal Methods in System Design, 2007, v:30, n:1, pp:5-28 [Journal]
Loop Summarization Using Abstract Transformers. [Citation Graph (, )][DBLP]
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. [Citation Graph (, )][DBLP]
Termination Analysis with Compositional Transition Invariants. [Citation Graph (, )][DBLP]
Symbolic Counter Abstraction for Concurrent Software. [Citation Graph (, )][DBLP]
Dynamic Cutoff Detection in Parameterized Concurrent Programs. [Citation Graph (, )][DBLP]
Coverage in interpolation-based model checking. [Citation Graph (, )][DBLP]
Fixed points for multi-cycle path detection. [Citation Graph (, )][DBLP]
Strengthening properties using abstraction refinement. [Citation Graph (, )][DBLP]
Lifting Propositional Interpolants to the Word-Level. [Citation Graph (, )][DBLP]
Mixed abstractions for floating-point arithmetic. [Citation Graph (, )][DBLP]
A Complete Bounded Model Checking Algorithm for Pushdown Systems. [Citation Graph (, )][DBLP]
Formal verification at higher levels of abstraction. [Citation Graph (, )][DBLP]
Race analysis for SystemC using model checking. [Citation Graph (, )][DBLP]
Embedded software verification: challenges and solutions. [Citation Graph (, )][DBLP]
Model checking concurrent linux device drivers. [Citation Graph (, )][DBLP]
Verifying C++ with STL containers via predicate abstraction. [Citation Graph (, )][DBLP]
Loopfrog: A Static Analyzer for ANSI-C Programs. [Citation Graph (, )][DBLP]
Finding Lean Induced Cycles in Binary Hypercubes. [Citation Graph (, )][DBLP]
Scoot: A Tool for the Analysis of SystemC Models. [Citation Graph (, )][DBLP]
Ranking Function Synthesis for Bit-Vector Relations. [Citation Graph (, )][DBLP]
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. [Citation Graph (, )][DBLP]
Boom: Taking Boolean Program Model Checking One Step Further. [Citation Graph (, )][DBLP]
Approximation Refinement for Interpolation-Based Model Checking. [Citation Graph (, )][DBLP]
Interpolant Strength. [Citation Graph (, )][DBLP]
Decision Procedures for the Grand Challenge. [Citation Graph (, )][DBLP]
Speeding Up Simulation of SystemC Using Model Checking. [Citation Graph (, )][DBLP]
Craig Interpolation for Quantifier-Free Presburger Arithmetic [Citation Graph (, )][DBLP]
Search in 0.062secs, Finished in 0.065secs
|