Natasha Sharygina's Publications

• Dynamic Component Substitutability Analysis , To appear in Proceedings of the Formal Methods (FM) 2005 conference , (with Edmund Clarke, Sagar Chaki and Nishant Sinha). New
  

• The ComFoRT Reasoning Framework, To appear in Proceedings of the Computer-Aided Verification (CAV) 2005 conference , (with Sagar Chaki, James Ivers and Kurt Wallnau). New
  

• COGENT: Accurate Theorem Proving for Program Verification, To appear in Proceedings of the Computer-Aided Verification (CAV) 2005 conference , (with Byron Cook and Daniel Kroening). New
  

• Symbolic Model Checking for Asynchronous Boolean Programs, To appear in Proceedings of the 12th International SPIN Workshop on Model Checking of Software , (with Byron Cook and Daniel Kroening). New
  

• SATABS: SAT-based Predicate Abstraction for ANSI-C , In Proceedings of the TACAS (Tools and Algorithms for the Construction and Analysis of Systems) 2005 International Conference , Lecture Notes in Computer Science 3440, p. 570 - 574 (with Edmund Clarke, Daniel Kroening and Karen Yorav).
  

• Accurate Theorem Proving for Program Verification , ETH Zurich Technical Report 473, 2005 (with Daniel Kroening and Byron Cook).
  

• Predicate Abstraction and Refinement Techniques for Verifying Verilog , To appear in Proceedings of the DAC (Design and Automation) 2005 International Conference , (with Edmund Clarke, Himanshu Jain and Daniel Kroening).
  

• Verification of Evolving Software , In Proceedings of the Specification and Verification of Component-based Systems (SAVCBS) Workshop, (with Sagar Chaki and Nishant Sinha).
  

• Overview of ComFoRT, A Model Checking Reasoning Framework , Carnegie Mellon University, Software Engineering Institute publications, CMU/SEI-2004-TN-0181, (with James Ivers).
  

• An Expressive Verification Framework for State/Event Systems , Submitted for publication, (with Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Tayssir Touili, and Helmut Veith).
  

• Automated, compositional and iterative deadlock detection , In Proceedings of the Second ACM-IEEE International Conference on Formal Methods for Codesign (MEMOCODE) 2004 , (with Sagar Chaki, Edmund Clarke, and Joel Ouaknine).
  

• State/Event-based Software Model Checking , In Proceedings of IFM (Integrated Formal Methods) 2004 International Conference , Lecture Notes in Computer Science 2999, p. 128 - 147 (with Sagar Chaki, Edmund Clarke, Joel Ouaknine, and Nishant Sinha).
  

• Predicate Abstraction of ANSI-C Programs using SAT , In the Formal Methods in System Design Journal , Vol. 25(2), p. 105 - 127, 2004. A conference version of the paper first appeared in the Proceedings of the Model Checking for Dependable Software-Intensive Systems Workshop of the International Conference on Dependable Systems and Networks 2003 , (with Edmund Clarke, Daniel Kroening, and Karen Yorav).
  

• Model Checking Software via Abstraction of Loop Transitions , In Proceedings of the Fundamental Approaches to Software Engineering: 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003 , Lecture Notes in Computer Science 2621, p. 325 - 340 (with James C. Browne).
  

• Lessons Learned from Model Checking a NASA Robot Controller , In the Formal Methods in System Design Journal , Vol. 25(3), p. 241 - 270, 2004. The paper was first presented at the SEI Software Model Checking Workshop, Pittsburgh, PA, USA, March, 2003 , (with James C. Browne, Robert Kurshan, Vladimir Levin, and Fei Xie).
  

• Model Checking of Software Control Systems , Ph.D. Dissertation, 2002, The University of Texas at Austin .
  

• Development of Verifiable Programs - Application of an Approach based on Executable Design Specifications , The University of Texas at Austin, Department of Computer Sciences, Technical Report TR-02-16 , 2002 (with James C. Browne, and Delbert Tesar).
  

• A Combined Testing and Verification Approach for Software Reliability , In the FME 2001: Formal Methods for Increasing Software Productivity: International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001 , Lecture Notes in Computer Science 2021, p. 611 - 628 (with Doron Peled).
  

• A Formal Object-Oriented Analysis for Software Reliability , In the Fundamental Approaches to Software Engineering : 4th International Conference, FASE 2001 : Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001 , Lecture Notes in Computer Science 2029, p. 318 - 322 (with James C. Browne, and Robert Kurshan).