Publications

A Model Checking-based Approach for Security Policy Verification of Mobile Systems, Braghin, C.; Sharygina, N.; Barone-Adesi, K. , Formal Aspects of Computing Journal, (2010)
Download:  bsb_facj2010.pdf 

A Flexible Schema for Generating Explanations in Lazy Theory Propagation, Bruttomesso, R.; Pek, E.; Sharygina, N. , International Conference on Formal Methods and Models for Codesign (MEMOCODE), Grenoble, France, (2010)
Download:  bps_memocode2010.pdf 

Flexible Interpolation with Local Proof Transformations, Bruttomesso, R.; Rollini, S.F.; Sharygina, N.; Tsitovich, A. , International Conference of Computer Aided Design (ICCAD), San Jose, USA, (2010)

The OpenSMT Solver, Bruttomesso, R.; Pek, E.; Sharygina, N.; Tsitovich, A. , International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6015, Paphos, Cyprus, p.150-153, (2010)
Download:  bpst2010.pdf 

Termination Analysis with Compositional Transition Invariants, Kroening, D.; Sharygina, N.; Tsitovich, A.; Wintersteiger, C.M. , International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, (2010)
Download:  kstw2010.pdf 

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

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

Loopfrog: A Static Analyzer for ANSI-C Programs, Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M. , The 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, p.668-670, (2009)
Download:  main.pdf 

The Synergy of Precise and Fast Abstractions for Program Verification, Sharygina, N.; Tonetta, S.; Tsitovich, A. , 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573, (2009)
Download:  stt2009.pdf 

Loop Summarization using Abstract Transformers, Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M. , 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 5311, Seoul, South Korea, p.111-125, (2008)
Download:  ksttw08.pdf 

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

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

Verification of evolving software via component substitutability analysis, Chaki, S.; Clarke, E.M.; Sharygina, N.; Sinha, N. , 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, Jain, H.; Kroening, D.; Sharygina, N.; Clarke, E.M. , 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, C.; Sharygina, N.; Barone-Adesi, K. , Integrated Formal Methods (IFM), Volume 4591, p.37-53, (2007)

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

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

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

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

Over-Approximating Boolean Programs with Unbounded Thread Creation., Cook, B.; Kroening, D.; Sharygina, N. , FMCAD, p.53-59, (2006)

Concurrent software verification with states, events, and deadlocks., Chaki, S.; Clarke, E.M.; Ouaknine, J.; Sharygina, N.; Sinha, N. , Formal Asp. Comput., Volume 17, Number 4, p.461-483, (2005)

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

Dynamic Component Substitutability Analysis., Sharygina, N.; Chaki, S.; Clarke, E.M.; Sinha, N. , Lecture Notes in Computer Science, Volume 3582, p.512-528, (2005)

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

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