Daniel Kroening : Publications
|
[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. |
|
[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. |
|
[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. |
|
[4] |
Numeric Bounds Analysis with Conflict−Driven Learning Vijay D'Silva‚ Leopold Haller‚ Daniel Kroening and Michael Tautschnig In TACAS. 2012. |
|
[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. |
|
[6] |
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 | BibTeX | DOI (10.1007/978-3-642-11319-2_12) | Link |
|
[7] |
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. |
|
[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. |
|
[9] |
Verification and Falsification of Programs with Loops Using Predicate Abstraction Daniel Kroening and Georg Weissenbacher In Formal Aspects of Computing. 2009. |
|
[10] |
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. |
|
[11] |
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. |
|
[12] |
Digitaltechnik Armin Biere‚ Daniel Kroening‚ Georg Weissenbacher and Christoph Wintersteiger Springer. March, 2008. |
|
[13] |
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. |
|
[14] |
Restructuring Resolution Refutations for Interpolation Vijay D'Silva‚ Daniel Kroening‚ Mitra Purandare and Georg Weissenbacher October, 2008. |
|
[15] |
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. |
|
[16] |
Decision Procedures – an Algorithmic Point of View Daniel Kroening and Ofer Strichman Springer. 2008. To appear |
|
[17] |
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. |
|
[18] |
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. |
|
[19] |
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. |
|
[20] |
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. |
|
[21] |
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. |
|
[22] |
Formal Verification at Higher Levels of Abstraction Daniel Kroening and Sanjit A. Seshia In Proceedings of ICCAD 2007. Pages 572–578. IEEE. 2007. Tutorial |
|
[23] |
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. |
|
[24] |
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. |
|
[25] |
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. |
|
[26] |
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) |
|
[27] |
SAT−based Summarisation for Boolean Programs Gerard Basler‚ Daniel Kroening and Georg Weissenbacher In Proceedings of SPIN 2007. No. 4595. Pages 131–148. 2007. |
|
[28] |
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. |
|
[29] |
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. |
|
[30] |
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. |
|
[31] |
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. |
|
[32] |
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. |
|
[33] |
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. |
|
[34] |
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. |
|
[35] |
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. |
|
[36] |
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. |
|
[37] |
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. |
|
[38] |
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. |
|
[39] |
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. |
|
[40] |
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. |
|
[41] |
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. |
|
[42] |
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. |
|
[43] |
Formal Verification of SystemC by Automatic Hardware/Software Partitioning Daniel Kroening and Natasha Sharygina In Proceedings of MEMOCODE 2005. Pages 101–110. IEEE. 2005. |
|
[44] |
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. |
|
[45] |
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. |
|
[46] |
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. |
|
[47] |
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. |
|
[48] |
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. |
|
[49] |
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. |
|
[50] |
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. |
|
[51] |
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. |
|
[52] |
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. |
|
[53] |
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. |
|
[54] |
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. |
|
[55] |
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. |
|
[56] |
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. |
|
[57] |
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. |
|
[58] |
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. |
|
[59] |
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. |
|
[60] |
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. |
|
[61] |
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. |
|
[62] |
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. |
|
[63] |
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. |
|
[64] |
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. |
|
[65] |
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. |
|
[66] |
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. |
|
[67] |
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. |