Publications

An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT, Roberto Bruttomesso , 7th International Workshop on Satisfiability Modulo Theories (SMT2009), Montreal, Canada, (2009)
Download:  dpfm.pdf 

A Scalable Decision Procedure for Fixed-Width Bit-Vectors, Roberto Bruttomesso, Natasha Sharygina , International Conference of Computer Aided Design, San Jose (CA), (2009)
Download:  iccad09.pdf 

Loopfrog: A Static Analyzer for ANSI-C Programs, Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger , The 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, (2009)
Download:  main.pdf 

The Synergy of Precise and Fast Abstractions for Program Verification, Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich , 24th Annual ACM Symposium on Applied Computing, Honolulu, Hawaii, USA, (2009)
Download:  stt2009.pdf 

Loop Summarization using Abstract Transformers, Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. , Proceedings of ATVA 2008, Seoul, South Korea, (2008)
Download:  ksttw08.pdf 

Detection of Security Vulnerabilities Using Guided Model Checking, Tsitovich, Aliaksei , 24th International Conference on Logic Programming, Udine, Italy, p.822 - 823, (2008)
Download:  ICLP08Tsitovich.pdf 

Scoot: A Tool for the Analysis of SystemC Models, Nicolas Blanc; Daniel Kroening; Natasha Sharygina , TACAS, p.467-470, (2008)
Download:  BlancKS08.pdf 

Verification of evolving software via component substitutability analysis, Sagar Chaki; Edmund M. Clarke; Natasha Sharygina; Nishant Sinha , Formal Methods in System Design, Volume 32, Number 3, p.235-266, (2008)
Download:  ChakiCSS08.pdf 

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog, Himanshu Jain; Daniel Kroening; Natasha Sharygina; Edmund M. Clarke , IEEE Trans. on CAD of Integrated Circuits and Systems, Volume 27, Number 2, p.366-379, (2008)
Download:  JainKSC08.pdf 

Automated Verification of Security Policies in Mobile Code., Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina , Lecture Notes in Computer Science, Volume 4591, p.37-53, (2007)

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs., Kroening, Daniel; Sharygina, Natasha , DATE, p.1325-1330, (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement., Jain, Himanshu; Kroening, Daniel; Sharygina, Natasha; Clarke, Edmund M. , Lecture Notes in Computer Science, Volume 4424, p.583-586, (2007)
Download:  vcegar-tool.pdf 

Model Checking with Abstraction for Web Services., Sharygina, Natasha; Kröning, Daniel , Test and Analysis of Web Services, p.121-145, (2007)

Approximating Predicate Images for Bit-Vector Logic., Kroening, Daniel; Sharygina, Natasha , Lecture Notes in Computer Science, Volume 3920, p.242-256, (2006)

Over-Approximating Boolean Programs with Unbounded Thread Creation., Cook, Byron; Kroening, Daniel; Sharygina, Natasha , FMCAD, p.53-59, (2006)

Concurrent software verification with states, events, and deadlocks., Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant , Formal Asp. Comput., Volume 17, Number 4, p.461-483, (2005)

Cogent: Accurate Theorem Proving for Program Verification., Cook, Byron; Kroening, Daniel; Sharygina, Natasha , Lecture Notes in Computer Science, Volume 3576, p.296-300, (2005)

Dynamic Component Substitutability Analysis., Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund M.; Sinha, Nishant , Lecture Notes in Computer Science, Volume 3582, p.512-528, (2005)

Formal verification of SystemC by automatic hardware/software partitioning., Kroening, Daniel; Sharygina, Natasha , MEMOCODE, p.101-110, (2005)

Program Compatibility Approaches., Clarke, Edmund M.; Sharygina, Natasha; Sinha, Nishant , Lecture Notes in Computer Science, Volume 4111, p.243-258, (2005)

State/Event Software Verification for Branching-Time Specifications., Chaki, Sagar; Clarke, Edmund M.; Grumberg, Orna; Ouaknine, Joël; Sharygina, Natasha; Touili, Tayssir; Veith, Helmut , Lecture Notes in Computer Science, Volume 3771, p.53-69, (2005)

Symbolic Model Checking for Asynchronous Boolean Programs., Cook, Byron; Kroening, Daniel; Sharygina, Natasha , Lecture Notes in Computer Science, Volume 3639, p.75-90, (2005)

SATABS: SAT-Based Predicate Abstraction for ANSI-C., Clarke, Edmund M.; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen , Lecture Notes in Computer Science, Volume 3440, p.570-574, (2005)

The ComFoRT Reasoning Framework., Chaki, Sagar; Ivers, James; Sharygina, Natasha; Wallnau, Kurt C. , Lecture Notes in Computer Science, Volume 3576, p.164-169, (2005)

Word level predicate abstraction and refinement for verifying RTL verilog., Jain, Himanshu; Kroening, Daniel; Sharygina, Natasha; Clarke, Edmund M. , DAC, p.445-450, (2005)