BOOKS

Book Chapters

• Bounded Model Checking
  A. Biere, A. Cimatti, Edmund Clarke, Ofer Strichman, Y. Zhu, 2003

• Behavioral Subtyping Using Invariants and Constraints
  Barbara H. Liskov, Jeannette M. Wing, 1999

• Hints to Specifiers
  Jeannette M. Wing, 1996

PAPERS

• Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling
  H.L.S. Younes, R.G. Simmons, 2002

• A Suite of Tools for Debugging Distributed Autonomous Systems
  D. Kortenkamp, T. Milam, R. Simmons, J. L. Fernandez, 2002

• SAT based Abstraction-Refinement using ILP and Machine Learning Techniques
  Edmund Clarke, A. Gupta, J. Kukula, Ofer Strichman, 2002

• Deciding Separation Formulas with SAT
  Ofer Strichman, S.A. Seshia, R.E. Bryant, 2002

• On solving Presburger and Linear Arithmetic with SAT
  Ofer Strichman, 2002

• A Failed attempt to Optimize Variable Ordering with Tools for Constraints Solving
  Edmund Clarke, Ofer Strichman, 2002

• Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling
  H.L.S. Younes, R.G. Simmons, 2002

• Digitisation and full abstraction for dense-time model checking
  Joel Ouaknine, 2002

• Timed CSP = Closed Timed Automata
  Joel Ouaknine, J. B. Worrell, 2002

• Universality and Language Inclusion for Open and Closed Timed Automata
  Joel Ouaknine, J. B. Worrell, 2003

• An intrinsic characterization of approximate probabilistic bisimilarity
  F. van Breugel, M. Mislove, Joel Ouaknine, J. B. Worrell, 2003

• Application Specific Higher Order Logic Theorem Proving
  Daniel Kroening, 2002

• Efficient Computation of Recurrence Diameters
  Daniel Kroening, Ofer Strichman, 2003

• Hardware Verification using ANSI-C Programs as a Reference
  Edmund Clarke, Daniel Kroening, 2003

• Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
  Daniel Kroening, Edmund Clarke, Karen Yorav, 2003

• Predicate Abstraction of ANSI-C Programs using SAT
  Edmund Clarke, Daniel Kroening, Natalia Sharygina, Karen Yorav, 2003

• Specifying and Verifying Systems with Multiple Clocks
  Edmund Clarke, Daniel Kroening, Karen Yorav, 2003

• Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor
  Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang Paul, 2003

• Completeness and Complexity of Bounded Model Checking
  Edmund Clarke, Daniel Kroening, Ofer Strichman, Joel Ouaknine, 2004

• A Tool for Checking ANSI-C Programs
  Edmund Clarke, Daniel Kroening, Flavio Lerda, 2004

• Predicate Abstraction of ANSI-C Programs using SAT
  Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav, 2004

• Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures
  Jennifer Morris, Daniel Kroening, Philip Koopman, 2004

• Abstraction-based Satisfiability Solving of Presburger Arithmetic
  Daniel Kroening, Joel Ouaknine, Sanjit Seshia, Ofer Strichman, 2004

• Abstraction-based Satisfiability Solving of Presburger Arithmetic
  Daniel Kroening, Joel Ouaknine, Sanjit Seshia, Ofer Strichman, 2004

• A SAT-Based Algorithm for Reparameterization in Symbolic Simulation
  Pankaj Chauhan, Edmund Clarke, Daniel Kroening, 2004

• Verification of SpecC and Verilog using Predicate Abstraction
  Edmund Clarke, Himanshu Jain, Daniel Kroening, 2004

• Understanding Counterexamples with explain
  Alex Groce, Daniel Kroening, Flavio Lerda, 2004

• Checking Consistency of C and Verilog using Predicate Abstraction and Induction
  Daniel Kroening, Edmund Clarke, 2004

• Making the Most of BMC Counterexamples
  Alex Groce, Daniel Kroening, 2005

• Counterexample Guided Abstraction Refinement via Program Execution
  Alex Groce, Daniel Kroening, 2004

• Computational Challenges in Bounded Model Checking
  Edmund Clarke, Daniel Kroening, Joel Ouaknine, Ofer Strichman, 2005

• SATABS: SAT-based Predicate Abstraction for ANSI-C
  Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav, 2005

• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
  Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund Clarke, 2005

• Cogent: Accurate theorem proving for program verification
  Byron Cook, Daniel Kroening, Natasha Sharygina, 2005

• Error Explanation with Distance Metrics
  Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman, 2005

• Putting it all together - Formal Verification of the VAMP
  Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul, 2006

• Formal Verification of SystemC by Automatic Hardware/Software Partitioning
  Daniel Kroening, Natasha Sharygina, 2005

• Symbolic model checking for asynchronous Boolean programs
  Byron Cook, Daniel Kroening, Natasha Sharygina, 2005

• Computing Over-Approximations with Bounded Model Checking
  Daniel Kroening, 2006

• Verification of SpecC using Predicate Abstraction
  Edmund Clarke, Himanshu Jain, Daniel Kroening, 2006

• Approximating Predicate Images for Bit-Vector Logic
  Daniel Kroening, Natasha Sharygina, 2006

• Accurate Theorem Proving for Program Verification
  Byron Cook, Daniel Kroening, Natasha Sharygina, 2006

• Counterexamples with Loops for Predicate Abstraction
  Daniel Kroening, Georg Weissenbacher, 2006

• Decision Procedures for the Grand Challenge
  Daniel Kroening, 2006

• Over-Approximating Boolean Programs with Unbounded Thread Creation
  Byron Cook, Daniel Kroening, Natasha Sharygina, 2006

• ExpliSAT: Guiding SAT-Based Software Verification with Explicit States
  Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz, 2006

• Formal Methods: State of the Art and Future Directions
  Edmund Clarke, Jeannette M. Wing, 1996

• A Symbiotic Relationship Between Formal Methods and Security
  Jeannette M. Wing, 1998

• Verifiable Secret Redistribution for Threshold Sharing Schemes
  Theodore M. Wong, Chenxi Wang Wang, Jeannette M. Wing, 2002

• Game Strategies in Network Security
  Kong-wei Lye, Jeannette M. Wing, 2002

• Automated Generation and Analysis of Attack Graphs
  Oleg Sheyner, Somesh Jha, Jeannette M. Wing, 2002

• Survivability Analysis of Networked Systems
  Somesh Jha and Jeannette M. Wing, 2001

• Composing Proofs of Security Protocols Using Isabelle/IOA
  Oleg Sheyner, Jeannette M. Wing, 2000

• A Comparison and Combination of Theory Generation and Model Checking for Security Protocol Analysis
  Nicholas J. Hopper, Sanjit A. Seshia, Jeannette M. Wing, 2000

• Survivability Analysis of Network Specifications
  Somesh Jha, Richard Linger, Tom Longstaff, Jeannette M. Wing, 2000

• A Nitpick Analysis of Mobile IPv6
  Daniel Jackson, Yuchung Ng, Jeannette M. Wing, 1998

• Fast, Automatic Checking of Security Protocols
  Darrell Kindred, Jeannette M. Wing, 1996

• A Case Study in Model Checking Software Systems
  Jeannette M. Wing, Mandana Vaziri-Farahani, 1997

• Respectful Type Converters
  Jeannette M. Wing, John Ockerbloom, 2000

• Respectful Type Converters For Mutable Types
  Jeannette M. Wing, John Ockerbloom, 1999

• Specification Matching Software Components
  Amy Moormann Zaremski, Jeannette M. Wing, 1997

• A Behavioral Notion of Subtyping
  Barbara H. Liskov, Jeannette M. Wing, 1994

• Mathematics in Computer Science Curricula (Abstract)
  Jeannette M. Wing, 2002

• Weaving Formal Methods into the Undergraduate Computer Science Curriculum (Extended Abstract)
  Jeannette M. Wing, 2000

• Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
  H{\aa}kan L. S. and Kwiatkowska, Marta and Norman, Gethin, and Parker, David Younes, 2004

Master/Phd Thesis

Other

• Optimizations in decision procedures for propositional linear inequalities
  Ofer Strichman, 2002

• Minimization and Reliability Analyses of Attack Graphs
  Somesh Jha, Oleg Sheyner, Jeannette M. Wing, 2002

• Theory Generation for Security Protocols
  Darrell Kindred, Jeannette M. Wing, 1999

We welcome feedback and comments at kroening@cs.cmu.edu.
Last modified by Daniel Kröning.