Daniel Kroening: Publications

[1]	Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT-Solvers Zinovik, Igor, Kroening, Daniel and Chebiryak, Yury IEEE Transactions on Information Theory, 2008. To appear. Details \| BibTeX

[2]	A Survey of Automated Techniques for Formal Software Verification D'Silva, Vijay, Kroening, Daniel and Weissenbacher, Georg IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Vol. 27, No. 7, pages 1165-1178. July 2008. Details \| BibTeX \| Link

[3]	Scoot: A Tool for the Analysis of SystemC Models Blanc, Nicolas, Kroening, Daniel and Sharygina, Natasha In Proceedings of TACAS 2008 Springer, 2008. To appear. Details \| BibTeX

[4]	Approximation Refinement for Interpolation-Based Model Checking D'Silva, Vijay, Purandare, Mitra and Kroening, Daniel In Proceedings of VMCAI 2008 Vol. 4905 of Lecture Notes in Computer Science, pages 68—82. Springer, 2008. Details \| BibTeX

[5]	Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog Jain, Himanshu et al. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Vol. 27, pages 366—379. February 2008. Details \| BibTeX

[6]	Digitaltechnik Biere, Armin et al. Springer. March 2008. Details \| BibTeX

[7]	Decision Procedures — an Algorithmic Point of View Kroening, Daniel, Strichman, Ofer Springer. 2008. To appear. Details \| BibTeX

[8]	Formal Verification at Higher Levels of Abstraction Kroening, Daniel, Seshia, Sanjit A. In Proceedings of ICCAD 2007 pages 572—578. IEEE, 2007. Tutorial. Details \| BibTeX

[9]	A Complete Bounded Model Checking Algorithm for Pushdown Systems Basler, Gerard, Kroening, Daniel and Weissenbacher, Georg In Proceedings of HVC 2007 Vol. 4899 of Lecture Notes in Computer Science, pages 202—217. Springer, 2007. Details \| BibTeX

[10]	Verifying C++ with STL Containers via Predicate Abstraction Blanc, Nicolas, Groce, Alex and Kroening, Daniel In 22nd IEEE International Conference on Automated Software Engineering (ASE) pages 521—524. IEEE, 2007. Details \| BibTeX

[11]	Model Checking Concurrent Linux Device Drivers Witkowski, Thomas et al. In 22nd IEEE International Conference on Automated Software Engineering (ASE) pages 501—504. IEEE, 2007. Details \| BibTeX

[12]	Static Analysis to Enhance the Power of Model Checking for Concurrent Software Clarke, Edmund, Kroening, Daniel and Reps, Thomas In Department of Defense Sponsored Information Security Research pages 349—360. Wiley. July 2007. Details \| BibTeX

[13]	Lifting Propositional Interpolants to the Word-Level Kroening, Daniel, Weissenbacher, Georg In Proceedings of FMCAD pages 85—89. IEEE, 2007. Details \| BibTeX

[14]	Verification of Boolean Programs with Unbounded Thread Creation Cook, Byron, Kroening, Daniel and Sharygina, Natasha Theoretical Computer Science (TCS), Vol. 388, pages 227—242. 2007. Details \| BibTeX

[15]	Model Checking with Abstraction for Web Services Sharygina, Natasha, Kroening, Daniel In Luciano Baresi, Elisabetta DiNitto, editors, Test and Analysis of Web Services pages 121—145. Springer. 2007. Details \| BibTeX

[16]	SAT-based Summarisation for Boolean Programs Basler, Gerard, Kroening, Daniel and Weissenbacher, Georg In Proceedings of SPIN 2007 No. 4595, pages 131—148. 2007. Details \| BibTeX

[17]

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

Zinovik, Igor, Kroening, Daniel and Chebiryak, Yury

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

Details | BibTeX

[18]	A First Step Towards a Unified Proof Checker for QBF Jussila, Toni et al. In Proceedings of SAT 2007 Vol. 4501 of Lecture Notes in Computer Science, pages 201—214. Springer, 2007. Details \| BibTeX

[19]	VCEGAR: Verilog CounterExample Guided Abstraction Refinement Jain, Himanshu et al. In Proceedings of TACAS 2007 Vol. 4424 of Lecture Notes in Computer Science, pages 583—586. Springer, 2007. Details \| BibTeX

[20]	Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs Kroening, Daniel, Sharygina, Natasha In Proceedings of DATE 2007 pages 1325—1330. 2007. Details \| BibTeX

[21]	Deciding Bit-Vector Arithmetic with Abstraction Bryant, Randal E. et al. In Proceedings of TACAS 2007 Vol. 4424 of Lecture Notes in Computer Science, pages 358—372. Springer, 2007. Details \| BibTeX

[22]	ExpliSAT: Guiding SAT-Based Software Verification with Explicit States Sharon Barner et al. In Proceedings of HVC 2006 Vol. 4383 of Lecture Notes in Computer Science, pages 138—154. Springer, 2007. Details \| BibTeX

[23]	Verification of SpecC using Predicate Abstraction Clarke, Edmund, Jain, Himanshu and Kroening, Daniel Formal Methods in System Design (FMSD), Vol. 30, No. 1, pages 5—28. February 2007. Details \| BibTeX

[24]	Over-Approximating Boolean Programs with Unbounded Thread Creation Cook, Byron, Kroening, Daniel and Sharygina, Natasha In Proceedings of FMCAD 2006 pages 53—59. IEEE, 2006. Details \| BibTeX

[25]	Accurate Theorem Proving for Program Verification Cook, Byron, Kroening, Daniel and Sharygina, Natasha In Proceedings of ISoLA 2004 Vol. 4313 of Lecture Notes in Computer Science, pages 96—114. Springer, 2006. Details \| BibTeX

[26]	Counterexamples with Loops for Predicate Abstraction Kroening, Daniel, Weissenbacher, Georg In Proceedings of CAV 2006 Vol. 4144 of Lecture Notes in Computer Science, pages 152—165. Springer, 2006. Details \| BibTeX

[27]	Approximating Predicate Images for Bit-Vector Logic Kroening, Daniel, Sharygina, Natasha In Proceedings of TACAS 2006 Vol. 3920 of Lecture Notes in Computer Science, pages 242—256. Springer, 2006. Details \| BibTeX

[28]	Computing Over-Approximations with Bounded Model Checking Kroening, Daniel In Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005) Vol. 144 of ENTCS, pages 79—92. Elsevier, January 2006. Details \| BibTeX

[29]	Error Explanation with Distance Metrics Groce, Alex et al. Software Tools for Technology Transfer (STTT), Vol. 8, pages 229—247. June 2006. Details \| BibTeX

[30]	Putting it all together - Formal Verification of the VAMP Beyer, Sven et al. 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 \| BibTeX

[31]	Formal Verification of SystemC by Automatic Hardware/Software Partitioning Kroening, Daniel, Sharygina, Natasha In Proceedings of MEMOCODE 2005 pages 101—110. IEEE, 2005. Details \| BibTeX

[32]	Symbolic model checking for asynchronous Boolean programs Cook, Byron, Kroening, Daniel and Sharygina, Natasha In P. Godefroid, editor, Proceedings of SPIN 2005 No. 3639, pages 75—90. Springer, 2005. Details \| BibTeX

[33]	Cogent: Accurate theorem proving for program verification Cook, Byron, Kroening, Daniel and Sharygina, Natasha In Etessami, Kousha, Rajamani, Sriram K., editors, Proceedings of CAV 2005 Vol. 3576 of Lecture Notes in Computer Science. Springer, 2005. Details \| BibTeX

[34]	Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog Jain, Himanshu et al. In Proceedings of DAC 2005 pages 445—450. 2005. Details \| BibTeX

[35]	SATABS: SAT-based Predicate Abstraction for ANSI-C Clarke, Edmund et al. 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 \| BibTeX

[36]	Computational Challenges in Bounded Model Checking Clarke, Edmund et al. Software Tools for Technology Transfer (STTT), Vol. 7, No. 2, pages 174—183. 2005. Details \| BibTeX

[37]	Making the Most of BMC Counterexamples Groce, Alex, Kroening, Daniel In Proceedings of BMC 2004 Vol. 119 of ENTCS, pages 67—81. Elsevier, 2005. Details \| BibTeX

[38]	Predicate Abstraction of ANSI—C Programs using SAT Clarke, Edmund et al. Formal Methods in System Design (FMSD), Vol. 25, pages 105—127. 2004. Details \| BibTeX

[39]	Counterexample Guided Abstraction Refinement via Program Execution Groce, Alex, Kroening, Daniel In Proceedings of ICFEM 2004 No. 3308, pages 224—238. Springer, November 2004. Details \| BibTeX

[40]	Checking Consistency of C and Verilog using Predicate Abstraction and Induction Kroening, Daniel, Clarke, Edmund In Proceedings of ICCAD pages 66—72. IEEE, November 2004. Details \| BibTeX

[41]	Abstraction-based Satisfiability Solving of Presburger Arithmetic Kroening, Daniel et al. In Rajeev Alur, Doron A. Peled, editors, Proceedings of CAV 2004 No. 3114, pages 308—320. July 2004. Details \| BibTeX

[42]	Understanding Counterexamples with explain Groce, Alex, Kroening, Daniel and Lerda, Flavio In Rajeev Alur, Doron A. Peled, editors, Proceedings of CAV 2004 No. 3114, pages 453—456. July 2004. Details \| BibTeX

[43]	Verification of SpecC and Verilog using Predicate Abstraction Jain, Himanshu, Clarke, Edmund and Kroening, Daniel In Proceedings of MEMOCODE 2004 pages 7—16. IEEE, 2004. Details \| BibTeX

[44]	A SAT-Based Algorithm for Reparameterization in Symbolic Simulation Chauhan, Pankaj, Clarke, Edmund and Kroening, Daniel In Proceedings of DAC 2004 pages 524—529. ACM Press, 2004. Details \| BibTeX

[45]

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

Morris, Jennifer, Kroening, Daniel and Koopman, Philip

In Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004) pages 349—358. IEEE, 2004.

Details | BibTeX

[46]

A Tool for Checking ANSI-C Programs

Clarke, Edmund, Kroening, Daniel and Lerda, Flavio

In Kurt Jensen, 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 | BibTeX

[47]	Completeness and Complexity of Bounded Model Checking Clarke, Edmund et al. In 5th International Conference on Verification, Model Checking, and Abstract Interpretation Vol. 2937 of Lecture Notes in Computer Science, pages 85—96. 2004. Details \| BibTeX

[48]	Specifying and Verifying Systems with Multiple Clocks Clarke, Edmund, Kroening, Daniel and Yorav, Karen In Proc. of the 2003 International Conference on Computer Design (ICCD) pages 48—55. IEEE, October 2003. Details \| BibTeX

[49]

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

Beyer, Sven et al.

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

[50]	Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking Kroening, Daniel, Clarke, Edmund and Yorav, Karen In Proceedings of DAC 2003 pages 368—371. ACM Press, 2003. Details \| BibTeX

[51]	Hardware Verification using ANSI-C Programs as a Reference Clarke, Edmund, Kroening, Daniel In Proceedings of ASP-DAC 2003 pages 308—311. IEEE Computer Society Press, January 2003. Details \| BibTeX

[52]

Efficient Computation of Recurrence Diameters

Kroening, Daniel, Strichman, Ofer

In Zuck, L. et al. , 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 | BibTeX

[53]	Automated Pipeline Design Kroening, Daniel, Paul, Wolfgang In Proc. of 38th ACM/IEEE Design Automation Conference (DAC 2001) pages 810—815. ACM Press, 2001. Details \| BibTeX

[54]	Proving the Correctness of Processors with Delayed Branch using Delayed PC Mueller, Silvia M., Paul, Wolfgang and Kroening, Daniel In Althoefer, I. et al. , editors, Numbers, Information and Complexity pages 579—588. Kluwer, 2000. Details \| BibTeX

[55]

Proving the Correctness of Pipelined Micro-Architectures

Kroening, Daniel, Paul, Wolfgang and Mueller, Silvia M.

In Waldschmidt, Klaus, Grimm, Christoph, 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 | BibTeX

[56]	The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs. Mueller, Silvia M. et al. In In Proc. 15th GI/ITG conference 'Architektur von Rechensystemen' ARCS'99 pages 65—73. 1999. Details \| BibTeX