Daniel Kroening : Publications

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

Digitaltechnik

Armin Biere‚ Daniel Kroening‚ Georg Weissenbacher and Christoph Wintersteiger

Springer. March, 2008.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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