Publications

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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