Publications

Using Cross-Entropy for Satisfiability, Chockler, H.; Ivrii, A.; Matsliah, A.; Rollini, S.F.; Sharygina, N. , 28th Symposium On Applied Computing (SAC), to appear
Download:  cims13_draft.pdf 

eVolCheck: Incremental Upgrade Checker for C, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer (2013), to appear
Download:  TACAS2013.pdf 

An abstraction refinement approach combining precise and approximated techniques, Sharygina, N.; Tonetta, S.; Tsitovich, A. , International Journal on Software Tools for Technology Transfer (STTT), Volume 14, Issue 1, p.1-14, Springer (2012)
Download:  stt11_draft.pdf 

FunFrog: Bounded Model Checking with Interpolation-based Function Summarization, Sery, O.; Fedyukovich, G.; Sharygina, N. , Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India (2012)
Download:  atva2012.pdf 

Incremental Upgrade Checking by Means of Interpolation-based Function Summaries, Sery, O.; Fedyukovich, G.; Sharygina, N. , Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD), Cambridge, UK (2012)
Download:  fmcad2012.pdf 

Lazy Abstraction with Interpolants for Arrays, Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N. , 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), Mérida, Venezuela, Springer (2012)
Download:  ABGRS_LPAR.pdf 

Leveraging Interpolant Strength in Model Checking, Rollini, S.F.; Sery, O.; Sharygina, N. , 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, Springer (2012)
Download:  main.pdf 

SAFARI: SMT-based Abstraction For Arrays with Interpolants, Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N. , 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, Springer (2012)
Download:  ABGRS_CAV12.pdf 

Function Summaries in Software Upgrade Checking, Fedyukovich, G.; Sery, O.; Sharygina, N. , Haifa Verification Conference (HVC), Volume 7261, Haifa, Israel, Springer (2011)
Download:  hvcse2011.pdf  HVC2011 Ondrej Sery.pdf 

Interpolation-based Function Summaries in Bounded Model Checking, Sery, O.; Fedyukovich, G.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2011)
Download:  hvc2011.pdf 

Loop Summarization and Termination Analysis, Tsitovich, A.; Sharygina, N.; Wintersteiger, C.M.; Kroening, D. , International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6605, Saarbrücken, Germany, p.81-95, Springer (2011)
Download:  tswk11.pdf 

Scalable Abstractions for Efficient Security Checks, Tsitovich, A. , Faculty of Informatics, Lugano, p.164, University of Lugano (2011)
Download:  Aliaksei_Tsitovich_PhD_Thesis.pdf 

A Model Checking-based Approach for Security Policy Verification of Mobile Systems, Braghin, C.; Sharygina, N.; Barone-Adesi, K. , Formal Aspects of Computing Journal, Springer (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, IEEE Computer Society (2010)
Download:  bps_memocode2010.pdf 

An Efficient and Flexible Approach to Resolution Proof Reduction, Rollini, S.F.; Bruttomesso, R.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2010)
Download:  rbs10.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, IEEE Computer Society (2010)
Download:  brst10.pdf 

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, Springer (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, p.89-103, Springer (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, ACM (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), ACM (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, IEEE Computer Society (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, ACM (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, Springer (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, Springer (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