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.
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