Daniel Kroening : Publications

Books

• [1]

  Digitaltechnik

  Armin Biere‚ Daniel Kroening‚ Georg Weissenbacher and Christoph Wintersteiger

  Springer. March, 2008.

  Details about Digitaltechnik | BibTeX data for Digitaltechnik | Link to Digitaltechnik

• [2]

  Decision Procedures – an Algorithmic Point of View

  Daniel Kroening and Ofer Strichman

  Springer. 2008.

  To appear

  Details about Decision Procedures – an Algorithmic Point of View | BibTeX data for Decision Procedures – an Algorithmic Point of View

Book chapters

• [1]

  Static Analysis to Enhance the Power of Model Checking for Concurrent Software

  Edmund Clarke‚ Daniel Kroening and Thomas Reps

  In Department of Defense Sponsored Information Security Research. Pages 349–360. Wiley. July, 2007.

  Details about Static Analysis to Enhance the Power of Model Checking for Concurrent Software | BibTeX data for Static Analysis to Enhance the Power of Model Checking for Concurrent Software

• [2]

  Model Checking with Abstraction for Web Services

  Natasha Sharygina and Daniel Kroening

  In Luciano Baresi and Elisabetta DiNitto, editors, Test and Analysis of Web Services. Pages 121–145. Springer. 2007.

  Details about Model Checking with Abstraction for Web Services | BibTeX data for Model Checking with Abstraction for Web Services

Journal papers

• [1]

  Automated formal synthesis of provably safe digital controllers for continuous plants

  Alessandro Abate‚ Iury Bessa‚ Lucas Cordeiro‚ Cristina David‚ Pascal Kesseli‚ Daniel Kroening and Elizabeth Polgreen

  In Acta Informatica. December, 2019.

  Details about Automated formal synthesis of provably safe digital controllers for continuous plants | BibTeX data for Automated formal synthesis of provably safe digital controllers for continuous plants | DOI (10.1007/s00236-019-00359-1)

• [2]

  Kayak: Safe Semantic Refactoring to Java Streams

  Cristina David‚ Pascal Kesseli and Daniel Kroening

  In CoRR. Vol. abs/1712.07388. 2017.

  Details about Kayak: Safe Semantic Refactoring to Java Streams | BibTeX data for Kayak: Safe Semantic Refactoring to Java Streams | Link to Kayak: Safe Semantic Refactoring to Java Streams

• [3]

  Verification and Falsification of Programs with Loops Using Predicate Abstraction

  Daniel Kroening and Georg Weissenbacher

  In Formal Aspects of Computing. 2009.

  Details about Verification and Falsification of Programs with Loops Using Predicate Abstraction | BibTeX data for Verification and Falsification of Programs with Loops Using Predicate Abstraction | DOI (10.1007/s00165-009-0110-2) | Link to Verification and Falsification of Programs with Loops Using Predicate Abstraction

• [4]

  Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT−Solvers

  Igor Zinovik‚ Daniel Kroening and Yury Chebiryak

  In IEEE Transactions on Information Theory. April, 2008.

  To appear.

  Details about Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT−Solvers | BibTeX data for Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT−Solvers

• [5]

  A Survey of Automated Techniques for Formal Software Verification

  Vijay D'Silva‚ Daniel Kroening and Georg Weissenbacher

  In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD). Vol. 27. No. 7. Pages 1165−1178. July, 2008.

  Details about A Survey of Automated Techniques for Formal Software Verification | BibTeX data for A Survey of Automated Techniques for Formal Software Verification | DOI (10.1109/TCAD.2008.923410) | Link to A Survey of Automated Techniques for Formal Software Verification

• [6]

  Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

  Himanshu Jain‚ Daniel Kroening‚ Natasha Sharygina and Edmund Clarke

  In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD). Vol. 27. Pages 366–379. February, 2008.

  Details about Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog | BibTeX data for Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

• [7]

  Verification of Boolean Programs with Unbounded Thread Creation

  Byron Cook‚ Daniel Kroening and Natasha Sharygina

  In Theoretical Computer Science (TCS). Vol. 388. Pages 227–242. 2007.

  Details about Verification of Boolean Programs with Unbounded Thread Creation | BibTeX data for Verification of Boolean Programs with Unbounded Thread Creation

• [8]

  Verification of SpecC using Predicate Abstraction

  Edmund Clarke‚ Himanshu Jain and Daniel Kroening

  In Formal Methods in System Design (FMSD). Vol. 30. No. 1. Pages 5–28. February, 2007.

  Details about Verification of SpecC using Predicate Abstraction | BibTeX data for Verification of SpecC using Predicate Abstraction

• [9]

  Error Explanation with Distance Metrics

  Alex Groce‚ Sagar Chaki‚ Daniel Kroening and Ofer Strichman

  In Software Tools for Technology Transfer (STTT). Vol. 8. Pages 229–247. June, 2006.

  Details about Error Explanation with Distance Metrics | BibTeX data for Error Explanation with Distance Metrics

• [10]

  Putting it all together − Formal Verification of the VAMP

  Sven Beyer‚ Christian Jacobi‚ Daniel Kroening‚ Dirk Leinenbach and Wolfgang J. Paul

  In Software Tools for Technology Transfer (STTT)‚ Special Issue on Recent Advances in Hardware Verification. Vol. 8. No. 4−5. Pages 411–430. August, 2006.

  Details about Putting it all together − Formal Verification of the VAMP | BibTeX data for Putting it all together − Formal Verification of the VAMP

• [11]

  Computational Challenges in Bounded Model Checking

  Edmund Clarke‚ Daniel Kroening‚ Joel Ouaknine and Ofer Strichman

  In Software Tools for Technology Transfer (STTT). Vol. 7. No. 2. Pages 174–183. April, 2005.

  Details about Computational Challenges in Bounded Model Checking | BibTeX data for Computational Challenges in Bounded Model Checking

• [12]

  Predicate Abstraction of ANSI–C Programs using SAT

  Edmund Clarke‚ Daniel Kroening‚ Natasha Sharygina and Karen Yorav

  In Formal Methods in System Design (FMSD). Vol. 25. Pages 105–127. 2004.

  Details about Predicate Abstraction of ANSI–C Programs using SAT | BibTeX data for Predicate Abstraction of ANSI–C Programs using SAT

Conference papers

• [1]

  Abstract Conflict Driven Learning

  V. D'Silva‚ L. Haller and D. Kroening

  In Proc. of the Symposium on Principles of Programming Languages. ACM. 2013.

  Details about Abstract Conflict Driven Learning | BibTeX data for Abstract Conflict Driven Learning

• [2]

  Abstraction of Syntax

  V. D'Silva and D. Kroening

  In Proc. of the conference on Verification‚ Model Checking and Abstract Interpretation. Springer−Verlag. 2013.

  Details about Abstraction of Syntax | BibTeX data for Abstraction of Syntax

• [3]

  An Abstract Interpretation of DPLL(T)

  M. Brain‚ V. D'Silva‚ L. Haller‚ A. Griggio and D. Kroening

  In Proc. of the conference on Verification‚ Model Checking and Abstract Interpretation. 2013.

  Details about An Abstract Interpretation of DPLL(T) | BibTeX data for An Abstract Interpretation of DPLL(T)

• [4]

  Numeric Bounds Analysis with Conflict−Driven Learning

  Vijay D'Silva‚ Leopold Haller‚ Daniel Kroening and Michael Tautschnig

  In TACAS. 2012.

  Details about Numeric Bounds Analysis with Conflict−Driven Learning | BibTeX data for Numeric Bounds Analysis with Conflict−Driven Learning | Download (pdf) of Numeric Bounds Analysis with Conflict−Driven Learning

• [5]

  Satisfiability Solvers are Static Analysers

  V. D'Silva‚ L. Haller and D. Kroening

  In Proc. of Static Analysis Symposium. Pages 317−333. Springer. 2012.

  Details about Satisfiability Solvers are Static Analysers | BibTeX data for Satisfiability Solvers are Static Analysers

• [6]

  An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions

  Daniel Kroening and Georg Weissenbacher

  In Kedar Namjoshi and Andreas Zeller, editors, Proceedings of the 5th Haifa Verification Conference. Springer. 2010.

  This work was also presented at the UNU IIST seminar in Macau (click here for slides) in January 2010.

  Details about An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions | BibTeX data for An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions

• [7]

  Interpolant Strength

  Vijay D'Silva‚ Daniel Kroening‚ Mitra Purandare and Georg Weissenbacher

  In Proceedings of the International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI). Vol. 5944 of Lecture Notes in Computer Science. Pages 129−145. Springer. January, 2010.

  Extended version available as technical report. Download slides.

  Details about Interpolant Strength | BibTeX data for Interpolant Strength | DOI (10.1007/978-3-642-11319-2_12) | Link to Interpolant Strength

• [8]

  Fixed Points in Multi−Cycle Path Detection

  Vijay D'Silva and Daniel Kroening

  In Bashir Al−Hashimi, editor, Proceedings of the Conference on Design Automation and Test in Europe (DATE). IEEE. April, 2009.

  Details about Fixed Points in Multi−Cycle Path Detection | BibTeX data for Fixed Points in Multi−Cycle Path Detection

• [9]

  Approximation Refinement for Interpolation−Based Model Checking

  Vijay D'Silva‚ Mitra Purandare and Daniel Kroening

  In Francesco Logozzo‚ Doron Peled and Lenore D. Zuck, editors, Proceedings of the International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI). Vol. 4905 of Lecture Notes in Computer Science. Pages 68–82. Heidelberg‚ Germany. January, 2008. Springer.

  Details about Approximation Refinement for Interpolation−Based Model Checking | BibTeX data for Approximation Refinement for Interpolation−Based Model Checking | DOI (10.1007/978-3-540-78163-9) | Link to Approximation Refinement for Interpolation−Based Model Checking

• [10]

  Scoot: A Tool for the Analysis of SystemC Models

  Nicolas Blanc‚ Daniel Kroening and Natasha Sharygina

  In Proceedings of TACAS 2008. Springer. 2008.

  To appear.

  Details about Scoot: A Tool for the Analysis of SystemC Models | BibTeX data for Scoot: A Tool for the Analysis of SystemC Models

• [11]

  Approximation Refinement for Interpolation−Based Model Checking

  Vijay D'Silva‚ Mitra Purandare and Daniel Kroening

  In Proceedings of VMCAI 2008. Vol. 4905 of Lecture Notes in Computer Science. Pages 68–82. Springer. 2008.

  Details about Approximation Refinement for Interpolation−Based Model Checking | BibTeX data for Approximation Refinement for Interpolation−Based Model Checking

• [12]

  Formal Verification at Higher Levels of Abstraction

  Daniel Kroening and Sanjit A. Seshia

  In Proceedings of ICCAD 2007. Pages 572–578. IEEE. 2007.

  Tutorial

  Details about Formal Verification at Higher Levels of Abstraction | BibTeX data for Formal Verification at Higher Levels of Abstraction

• [13]

  A Complete Bounded Model Checking Algorithm for Pushdown Systems

  Gerard Basler‚ Daniel Kroening and Georg Weissenbacher

  In Proceedings of HVC 2007. Vol. 4899 of Lecture Notes in Computer Science. Pages 202–217. Springer. 2007.

  Details about A Complete Bounded Model Checking Algorithm for Pushdown Systems | BibTeX data for A Complete Bounded Model Checking Algorithm for Pushdown Systems

• [14]

  Verifying C++ with STL Containers via Predicate Abstraction

  Nicolas Blanc‚ Alex Groce and Daniel Kroening

  In 22nd IEEE International Conference on Automated Software Engineering (ASE). Pages 521–524. IEEE. 2007.

  Details about Verifying C++ with STL Containers via Predicate Abstraction | BibTeX data for Verifying C++ with STL Containers via Predicate Abstraction

• [15]

  Model Checking Concurrent Linux Device Drivers

  Thomas Witkowski‚ Nicolas Blanc‚ Georg Weissenbacher and Daniel Kroening

  In 22nd IEEE International Conference on Automated Software Engineering (ASE). Pages 501–504. IEEE. 2007.

  Details about Model Checking Concurrent Linux Device Drivers | BibTeX data for Model Checking Concurrent Linux Device Drivers | DOI (10.1145/1321631.1321719) | Link to Model Checking Concurrent Linux Device Drivers

• [16]

  Lifting Propositional Interpolants to the Word−Level

  Daniel Kroening and Georg Weissenbacher

  In Proceedings of FMCAD. Pages 85–89. IEEE. 2007.

  (also presented in the TRESOR seminar at EPFL‚ June 2008)

  Details about Lifting Propositional Interpolants to the Word−Level | BibTeX data for Lifting Propositional Interpolants to the Word−Level | Link to Lifting Propositional Interpolants to the Word−Level

• [17]

  SAT−based Summarisation for Boolean Programs

  Gerard Basler‚ Daniel Kroening and Georg Weissenbacher

  In Proceedings of SPIN 2007. No. 4595. Pages 131–148. 2007.

  Click here for slides.

  Details about SAT−based Summarisation for Boolean Programs | BibTeX data for SAT−based Summarisation for Boolean Programs | Link to SAT−based Summarisation for Boolean Programs

• [18]

  An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits along Cyclic Attractors

  Igor Zinovik‚ Daniel Kroening and Yury Chebiryak

  In Proceedings of Algebraic Biology (AB). Vol. 4545 of Lecture Notes in Computer Science. Pages 140–154. Springer. 2007.

  Details about An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits along Cyclic Attractors | BibTeX data for An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits along Cyclic Attractors

• [19]

  A First Step Towards a Unified Proof Checker for QBF

  Toni Jussila‚ Armin Biere‚ Carsten Sinz‚ Daniel Kroening and Christoph Wintersteiger

  In Proceedings of SAT 2007. Vol. 4501 of Lecture Notes in Computer Science. Pages 201–214. Springer. 2007.

  Details about A First Step Towards a Unified Proof Checker for QBF | BibTeX data for A First Step Towards a Unified Proof Checker for QBF

• [20]

  VCEGAR: Verilog CounterExample Guided Abstraction Refinement

  Himanshu Jain‚ Daniel Kroening‚ Natasha Sharygina and Edmund Clarke

  In Proceedings of TACAS 2007. Vol. 4424 of Lecture Notes in Computer Science. Pages 583–586. Springer. 2007.

  Details about VCEGAR: Verilog CounterExample Guided Abstraction Refinement | BibTeX data for VCEGAR: Verilog CounterExample Guided Abstraction Refinement

• [21]

  Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs

  Daniel Kroening and Natasha Sharygina

  In Proceedings of DATE 2007. Pages 1325–1330. 2007.

  Details about Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs | BibTeX data for Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs

• [22]

  Deciding Bit−Vector Arithmetic with Abstraction

  Randal E. Bryant‚ Daniel Kroening‚ Joel Ouaknine‚ Sanjit A. Seshia‚ Ofer Strichman and Bryan Brady

  In Proceedings of TACAS 2007. Vol. 4424 of Lecture Notes in Computer Science. Pages 358–372. Springer. 2007.

  Details about Deciding Bit−Vector Arithmetic with Abstraction | BibTeX data for Deciding Bit−Vector Arithmetic with Abstraction

• [23]

  ExpliSAT: Guiding SAT−Based Software Verification with Explicit States

  Sharon Barner‚ Cindy Eisner‚ Ziv Glazberg‚ Daniel Kroening and Ishai Rabinovitz

  In Proceedings of HVC 2006. Vol. 4383 of Lecture Notes in Computer Science. Pages 138–154. Springer. 2007.

  Details about ExpliSAT: Guiding SAT−Based Software Verification with Explicit States | BibTeX data for ExpliSAT: Guiding SAT−Based Software Verification with Explicit States

• [24]

  Over−Approximating Boolean Programs with Unbounded Thread Creation

  Byron Cook‚ Daniel Kroening and Natasha Sharygina

  In Proceedings of FMCAD 2006. Pages 53–59. IEEE. 2006.

  Details about Over−Approximating Boolean Programs with Unbounded Thread Creation | BibTeX data for Over−Approximating Boolean Programs with Unbounded Thread Creation

• [25]

  Accurate Theorem Proving for Program Verification

  Byron Cook‚ Daniel Kroening and Natasha Sharygina

  In Proceedings of ISoLA 2004. Vol. 4313 of Lecture Notes in Computer Science. Pages 96–114. Springer. 2006.

  Details about Accurate Theorem Proving for Program Verification | BibTeX data for Accurate Theorem Proving for Program Verification

• [26]

  Counterexamples with Loops for Predicate Abstraction

  Daniel Kroening and Georg Weissenbacher

  In Proceedings of CAV 2006. Vol. 4144 of Lecture Notes in Computer Science. Pages 152–165. Springer. 2006.

  Details about Counterexamples with Loops for Predicate Abstraction | BibTeX data for Counterexamples with Loops for Predicate Abstraction | DOI (10.1007/11817963_16) | Link to Counterexamples with Loops for Predicate Abstraction

• [27]

  Approximating Predicate Images for Bit−Vector Logic

  Daniel Kroening and Natasha Sharygina

  In Proceedings of TACAS 2006. Vol. 3920 of Lecture Notes in Computer Science. Pages 242–256. Springer. 2006.

  Details about Approximating Predicate Images for Bit−Vector Logic | BibTeX data for Approximating Predicate Images for Bit−Vector Logic

• [28]

  Computing Over−Approximations with Bounded Model Checking

  Daniel Kroening

  In Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005). Vol. 144 of ENTCS. Pages 79–92. Elsevier. January, 2006.

  Details about Computing Over−Approximations with Bounded Model Checking | BibTeX data for Computing Over−Approximations with Bounded Model Checking

• [29]

  Formal Verification of SystemC by Automatic Hardware/Software Partitioning

  Daniel Kroening and Natasha Sharygina

  In Proceedings of MEMOCODE 2005. Pages 101–110. IEEE. 2005.

  Details about Formal Verification of SystemC by Automatic Hardware/Software Partitioning | BibTeX data for Formal Verification of SystemC by Automatic Hardware/Software Partitioning

• [30]

  Symbolic model checking for asynchronous Boolean programs

  Byron Cook‚ Daniel Kroening and Natasha Sharygina

  In P. Godefroid, editor, Proceedings of SPIN 2005. No. 3639. Pages 75–90. Springer. 2005.

  Details about Symbolic model checking for asynchronous Boolean programs | BibTeX data for Symbolic model checking for asynchronous Boolean programs

• [31]

  Cogent: Accurate theorem proving for program verification

  Byron Cook‚ Daniel Kroening and Natasha Sharygina

  In Kousha Etessami and Sriram K. Rajamani, editors, Proceedings of CAV 2005. Vol. 3576 of Lecture Notes in Computer Science. Springer. 2005.

  Details about Cogent: Accurate theorem proving for program verification | BibTeX data for Cogent: Accurate theorem proving for program verification

• [32]

  Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

  Himanshu Jain‚ Daniel Kroening‚ Natasha Sharygina and Edmund Clarke

  In Proceedings of DAC 2005. Pages 445–450. 2005.

  Details about Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog | BibTeX data for Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

• [33]

  SATABS: SAT−based Predicate Abstraction for ANSI−C

  Edmund Clarke‚ Daniel Kroening‚ Natasha Sharygina and Karen Yorav

  In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005). Vol. 3440 of Lecture Notes in Computer Science. Pages 570–574. Springer. 2005.

  Details about SATABS: SAT−based Predicate Abstraction for ANSI−C | BibTeX data for SATABS: SAT−based Predicate Abstraction for ANSI−C

• [34]

  Making the Most of BMC Counterexamples

  Alex Groce and Daniel Kroening

  In Proceedings of BMC 2004. Vol. 119 of ENTCS. Pages 67–81. Elsevier. 2005.

  Details about Making the Most of BMC Counterexamples | BibTeX data for Making the Most of BMC Counterexamples

• [35]

  Counterexample Guided Abstraction Refinement via Program Execution

  Alex Groce and Daniel Kroening

  In Proceedings of ICFEM 2004. No. 3308. Pages 224–238. Springer. November, 2004.

  Details about Counterexample Guided Abstraction Refinement via Program Execution | BibTeX data for Counterexample Guided Abstraction Refinement via Program Execution

• [36]

  Checking Consistency of C and Verilog using Predicate Abstraction and Induction

  Daniel Kroening and Edmund Clarke

  In Proceedings of ICCAD. Pages 66–72. IEEE. November, 2004.

  Details about Checking Consistency of C and Verilog using Predicate Abstraction and Induction | BibTeX data for Checking Consistency of C and Verilog using Predicate Abstraction and Induction

• [37]

  Abstraction−based Satisfiability Solving of Presburger Arithmetic

  Daniel Kroening‚ Joel Ouaknine‚ Sanjit Seshia and Ofer Strichman

  In Rajeev Alur and Doron A. Peled, editors, Proceedings of CAV 2004. No. 3114. Pages 308–320. July, 2004.

  Details about Abstraction−based Satisfiability Solving of Presburger Arithmetic | BibTeX data for Abstraction−based Satisfiability Solving of Presburger Arithmetic

• [38]

  Understanding Counterexamples with explain

  Alex Groce‚ Daniel Kroening and Flavio Lerda

  In Rajeev Alur and Doron A. Peled, editors, Proceedings of CAV 2004. No. 3114. Pages 453–456. July, 2004.

  Details about Understanding Counterexamples with explain | BibTeX data for Understanding Counterexamples with explain

• [39]

  Verification of SpecC and Verilog using Predicate Abstraction

  Himanshu Jain‚ Edmund Clarke and Daniel Kroening

  In Proceedings of MEMOCODE 2004. Pages 7–16. IEEE. 2004.

  Details about Verification of SpecC and Verilog using Predicate Abstraction | BibTeX data for Verification of SpecC and Verilog using Predicate Abstraction

• [40]

  A SAT−Based Algorithm for Reparameterization in Symbolic Simulation

  Pankaj Chauhan‚ Edmund Clarke and Daniel Kroening

  In Proceedings of DAC 2004. Pages 524–529. ACM Press. 2004.

  Details about A SAT−Based Algorithm for Reparameterization in Symbolic Simulation | BibTeX data for A SAT−Based Algorithm for Reparameterization in Symbolic Simulation

• [41]

  Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures

  Jennifer Morris‚ Daniel Kroening and Philip Koopman

  In Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004). Pages 349–358. IEEE. 2004.

  Details about Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures | BibTeX data for Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures

• [42]

  A Tool for Checking ANSI−C Programs

  Edmund Clarke‚ Daniel Kroening and Flavio Lerda

  In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Vol. 2988 of Lecture Notes in Computer Science. Pages 168–176. Springer. 2004.

  Details about A Tool for Checking ANSI−C Programs | BibTeX data for A Tool for Checking ANSI−C Programs

• [43]

  Completeness and Complexity of Bounded Model Checking

  Edmund Clarke‚ Daniel Kroening‚ Ofer Strichman and Joel Ouaknine

  In 5th International Conference on Verification‚ Model Checking‚ and Abstract Interpretation. Vol. 2937 of Lecture Notes in Computer Science. Pages 85–96. 2004.

  Details about Completeness and Complexity of Bounded Model Checking | BibTeX data for Completeness and Complexity of Bounded Model Checking

• [44]

  Specifying and Verifying Systems with Multiple Clocks

  Edmund Clarke‚ Daniel Kroening and Karen Yorav

  In Proc. of the 2003 International Conference on Computer Design (ICCD). Pages 48–55. IEEE. October, 2003.

  Details about Specifying and Verifying Systems with Multiple Clocks | BibTeX data for Specifying and Verifying Systems with Multiple Clocks

• [45]

  Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor

  Sven Beyer‚ Christian Jacobi‚ Daniel Kroening‚ Dirk Leinenbach and Wolfgang Paul

  In Proc. of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Vol. 2860 of Lecture Notes in Computer Science. Pages 51–65. Springer. October, 2003.

  Details about Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor | BibTeX data for Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor

• [46]

  Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking

  Daniel Kroening‚ Edmund Clarke and Karen Yorav

  In Proceedings of DAC 2003. Pages 368–371. ACM Press. 2003.

  Details about Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking | BibTeX data for Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking

• [47]

  Hardware Verification using ANSI−C Programs as a Reference

  Edmund Clarke and Daniel Kroening

  In Proceedings of ASP−DAC 2003. Pages 308–311. IEEE Computer Society Press. January, 2003.

  Details about Hardware Verification using ANSI−C Programs as a Reference | BibTeX data for Hardware Verification using ANSI−C Programs as a Reference

• [48]

  Efficient Computation of Recurrence Diameters

  Daniel Kroening and Ofer Strichman

  In L. Zuck‚ P. Attie‚ A. Cortesi and S. Mukhopadhyay, editors, 4th International Conference on Verification‚ Model Checking‚ and Abstract Interpretation. Vol. 2575 of Lecture Notes in Computer Science. Pages 298–309. Springer. January, 2003.

  Details about Efficient Computation of Recurrence Diameters | BibTeX data for Efficient Computation of Recurrence Diameters

• [49]

  Automated Pipeline Design

  Daniel Kroening and Wolfgang Paul

  In Proc. of 38th ACM/IEEE Design Automation Conference (DAC 2001). Pages 810–815. ACM Press. 2001.

  Details about Automated Pipeline Design | BibTeX data for Automated Pipeline Design

• [50]

  Proving the Correctness of Processors with Delayed Branch using Delayed PC

  Silvia M. Mueller‚ Wolfgang Paul and Daniel Kroening

  In I. Althoefer‚ N. Cai‚ G. Dueck‚ L. Khachatrian‚ M. Pinsker‚ A. Sarkozy‚ I. Wegener and Zhang Z., editors, Numbers‚ Information and Complexity. Pages 579–588. Kluwer. 2000.

  Details about Proving the Correctness of Processors with Delayed Branch using Delayed PC | BibTeX data for Proving the Correctness of Processors with Delayed Branch using Delayed PC

• [51]

  Proving the Correctness of Pipelined Micro−Architectures

  Daniel Kroening‚ Wolfgang Paul and Silvia M. Mueller

  In Klaus Waldschmidt and Christoph Grimm, editors, Proc. of ITG/GI/GMM−Workshop ”Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”. Pages 89–98. VDE Verlag. 2000.

  Details about Proving the Correctness of Pipelined Micro−Architectures | BibTeX data for Proving the Correctness of Pipelined Micro−Architectures

• [52]

  The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs.

  Silvia M. Mueller‚ Holger Leister‚ Peter Dell‚ Nikolaus Gerteis and Daniel Kroening

  In In Proc. 15th GI/ITG conference 'Architektur von Rechensystemen' ARCS'99. Pages 65–73. 1999.

  Details about The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs. | BibTeX data for The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs.

Miscellaneous

• [1]

  Restructuring Resolution Refutations for Interpolation

  Vijay D'Silva‚ Daniel Kroening‚ Mitra Purandare and Georg Weissenbacher

  October, 2008.

  Details about Restructuring Resolution Refutations for Interpolation | BibTeX data for Restructuring Resolution Refutations for Interpolation | Download (pdf) of Restructuring Resolution Refutations for Interpolation