Natasha Sharygina

http://usi.to/fqf

Publications

Key publications (1)

Bruttomesso R., Pek E., Sharygina N., Tsitovich A. (2010) The OpenSMT Solver

Journal Article (20)

Sharygina N., Blicha M., Britikov K. (2025) Golem: a flexible and efficient solver for constrained Horn clauses, Formal Methods in System Design
Sharygina N., Otoni R. B., Marescotti M., Alt L., Eugster P. T., Hyvärinen A. (2023) A Solicitous Approach to Smart Contract Verification, ACM Transactions on Privacy and Security
Sharygina N., Asadi S., Blicha M., Hyvärinen A., Fedyukovich G. (2022) SMT-based verification of program changes through summary repair, Formal Methods in System Design
Sharygina N., Jancík P., Kofron J., Alt L., Fedyukovich G., Hyvärinen A. (2019) Exploiting partial variable assignment in interpolation-based model checking, Formal Methods in System Design
Sharygina N., Alberti F., Ghilardi S. (2017) A Framework for the Verification of Parameterized Infinite-state Systems, Fundamenta Informaticae
Sharygina N., Fedyukovich G., Sery O. (2017) Flexible SAT-based framework for incremental bounded upgrade checking, International Journal on Software Tools for Technology Transfer
Sharygina N., Rollini S. F., Bruttomesso R., Tsitovich A. (2014) Resolution proof transformation for compression and interpolation, Formal Methods in System Design
Sharygina N., Alberti F., Bruttomesso R., Tsitovich A. (2014) An extension of lazy abstraction with interpolation for programs with arrays, Formal Methods in System Design
Kröning D., Sharygina N., Tonetta S., Tsitovich A., Wintersteiger C. M. (2013) Loop summarization using state and transition invariants, Formal Methods in System Design, 42 (3)
Alberti F., Sharygina N. (2013) Abstraction and Acceleration in SMT-based Model-Checking for Array Programs, CoRR, abs/1304.4499
Rollini S. F., Sharygina N. (2012) Propositional Interpolation Systems for Model Checking, CoRR, abs/1212.4650
Sharygina N., Tonetta S., Tsitovich A. (2012) An abstraction refinement approach combining precise and approximated techniques, International Journal on Software Tools for Technology Transfer (STTT), 14
Braghin C., Sharygina N., Barone-Adesi K. (2010) A Model Checking-based Approach for Security Policy Verification of Mobile Systems, Formal Aspects of Computing Journal
Jain H., Kröning D., Sharygina N., Clarke E. M. (2008) Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog, IEEE Trans. on CAD of Integrated Circuits and Systems, 27 (2)
Chaki S., Clarke E. M., Sharygina N., Sinha N. (2008) Verification of evolving software via component substitutability analysis, Formal Methods in System Design, 32 (3)
Cook B., Kröning D., Sharygina N. (2007) Verification of Boolean programs with unbounded thread creation, Theor. Comput. Sci., 388 (1-3)
Sharygina N., Chaki S., Clark E., Ouaknine J., Sinha N. (2005) Concurrent software verification with states, events, and deadlocks, Formal Aspects of Computing
Sharygina N., Clarke E., Kroening D., Yorav K. (2004) Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design
Sharygina N., Browne J., Xie F., Kurshan R., Levin V. (2004) Lessons Learned from Model Checking a NASA Robot Controller, Formal Methods in System Design
Blicha M., Hyvärinen A., Kofroň J., Sharygina N., Using linear algebra in decomposition of Farkas interpolants, International journal on software tools for technology transfer, 24

Book (1)

Sharygina N., Kröning D. (2007) Model Checking with Abstraction for Web Services.. Springer. Test and Analysis of Web Services

Conference proceedings (1)

Fedyukovich G., Sery O., Sharygina N. (2011) Function Summaries in Software Upgrade Checking. Springer. Haifa, Israel

Article in conference proceedings (63)

Sharygina N., Britikov K., Zlatkin I., Fedyukovich G., Alt L. (2024) SolTG: A CHC-Based Solidity Test Case Generator. CAV. Montreal, QC, Canada. July 24-27, 2024
Sharygina N., Britikov K., Blicha M., Fedyukovich G. (2024) Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. FM 2024. Milan, Italy. September 9-13, 2024
Sharygina N., Blicha M., Britikov K. (2023) The Golem Horn Solver. CAV 2023. Paris, France. July 17-22, 2023
Sharygina N., Otoni R. B., Blicha M., Eugster P. T. (2023) CHC Model Validation with Proof Guarantees. IFM 2023. Leiden, The Netherlands. November 13-15, 2023
Sharygina N., Otoni R. B., Konnov I., Kukovec J., Eugster P. T. (2023) Symbolic Model Checking for TLA+ Made Faster. TACAS 2023. Paris, France. April 22-27, 2023
Sharygina N., Britikov K., Hyvärinen A. (2023) Picky CDCL: SMT-Solving with Flexible Literal Selection. VSTTE 2023. Ames, IA, USA. December 12-15, 2023
Sharygina N., Blicha M., Fedyukovich G., Hyvärinen A. (2022) Split Transition Power Abstraction for Unbounded Safety. FMCAD 2022. Trento, Italy. October 17-21, 2022
Sharygina N., Blicha M., Fedyukovich G., Hyvärinen A. (2022) Transition Power Abstractions for Deep Counterexample Detection. TACAS 2022. Munich, Germany. April 2-7, 2022
Sharygina N. (2022) SolCMC: Solidity Compiler's Model Checker. CAV 2022. Haifa, Israel. August 7-10, 2022
Sharygina N., Otoni R. B., Blicha M., Eugster P. T., Hyvärinen A. (2021) Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. 58th DAC 2021. San Francisco, CA, USA. December 5-9, 2021
Sharygina N., Hyvärinen A., Marescotti M. (2021) Lookahead in Partitioning SMT. 21st FMCAD 2021. New Haven, CT, USA. October 19-22, 2021
Sharygina N., Asadi S., Blicha M., Hyvärinen A., Fedyukovich G. (2020) Incremental Verification by SMT-based Summary Repair. 20th FMCAD 2020. Haifa, Israel. September 21-24, 2020
Sharygina N., Marescotti M., Otoni R. B., Alt L., Eugster P. T., Hyvärinen A. (2020) Accurate Smart Contract Verification Through Direct Modelling. 9th International Symposium on Leveraging Applications of Formal Methods Part III. ISoLA 2020. Rhodes, Greece. October 20-30, 2020
Sharygina N., Asadi S., Blicha M., Hyvärinen A., Fedyukovich G. (2020) Farkas-Based Tree Interpolation. 27th SAS 2020. Virtual Event. November 18-20, 2020
Sharygina N., Blicha M., Hyvärinen A., Marescotti M. (2020) A Cooperative Parallelization Approach for Property-Directed k-Induction. 21th VMCAI 2020. New Orleans, LA, USA. January 16-21, 2020
Sharygina N., Even-Mendoza K., Hyvärinen A., Chockler H. (2019) Lattice-based SMT for program verification. 17th MEMOCODE 2019. La Jolla, CA, USA. October 9-11, 2019
Sharygina N., Blicha M., Hyvärinen A., Kofron J. (2019) Decomposing Farkas Interpolants. 25th TACAS 2019. Prague, Czech Republic. April 6-11, 2019
Sharygina N., Marescotti M., Blicha M., Hyvärinen A., Asadi S. (2018) Computing Exact Worst-Case Gas Consumption for Smart Contracts. ISoLA 2018. Limassol, Cyprus. November 5-9, 2018
Sharygina N., Asadi S., Blicha M., Fedyukovich G., Hyvärinen A., Even-Mendoza K., Chockler H. (2018) Function Summarization Modulo Theories. 22nd LPAR 2018. Awassa, Ethiopia. 16-21 November 2018
Sharygina N., Hyvärinen A., Marescotti M., Sadigova P., Chockler H. (2018) Lookahead-Based SMT Solving. 22nd LPAR 2018. Awassa, Ethiopia. 16-21 November 2018
Sharygina N., Marescotti M., Hyvärinen A. (2018) SMTS: Distributed, Visualized Constraint Solving. 22nd LPAR 2018. Awassa, Ethiopia. 16-21 November 2018
Sharygina N., Even-Mendoza K., Asadi S., Hyvärinen A., Chockler H. (2018) Lattice-Based Refinement in Bounded Model Checking. 10th VSTTE 2018. Oxford, UK. July 18-19, 2018
Sharygina N., Hyvärinen A., Asadi S., Alt L. (2017) Duality-based interpolation for quantifier-free equalities and uninterpreted functions. 17th FMCAD 2017. Vienna, Austria. October 2-6, 2017
Sharygina N., Marescotti M., Gurfinkel A., Hyvärinen A. (2017) Designing parallel PDR. 17th FMCAD 2017. Vienna, Austria. October 2-6, 2017
Sharygina N., Alt L., Hyvärinen A. (2017) LRA Interpolants from No Man's Land. 13. Haifa Verification Conference 2017. Haifa, Israel. November 13-15, 2017
Sharygina N., Hyvärinen A., Asadi S., Even-Mendoza K., Fedyukovich G., Chockler H. (2017) Theory Refinement for Program Verification. 20th SAT 2017. Melbourne, VIC, Australia. August 28 - September 1, 2017
Sharygina N., Budakovic J., Marescotti M., Hyvärinen A. (2017) Visualising SMT-Based Parallel Constraint Solving. 15th SMT 2017. Heidelberg, Germany. July 22 - 23, 2017
Sharygina N., Alt L., Asadi S., Chockler H., Even-Mendoza K., Fedyukovich G., Hyvärinen A. (2017) HiFrog: SMT-based Function Summarization for Software Verification. 23rd TACAS 2017. Uppsala, Sweden. April 22-29, 2017
Sharygina N., Marescotti M., Hyvärinen A. (2016) Clause Sharing and Partitioning for Cloud-Based SMT Solving. 14th ATVA 2016. Chiba, Japan. October 17-20, 2016
Sharygina N., Fedyukovich G., Gurfinkel A. (2016) Property Directed Equivalence via Abstract Simulation. 28th CAV 2016. Toronto, ON, Canada. July 17-23, 2016
Sharygina N., Jancík P., Alt L., Fedyukovich G., Hyvärinen A., Kofron J. (2016) PVAIR: Partial Variable Assignment InterpolatoR. 19. FASE 2016. Eindhoven, The Netherlands. April 2-8, 2016
Sharygina N., Hyvärinen A., Marescotti M., Alt L. (2016) OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. 19th SAT 2016. Bordeaux, France. July 5-8, 2016
Sharygina N., Fedyukovich G., D'Iddio A. C., Hyvärinen A. (2015) Symbolic Detection of Assertion Dependencies for Bounded Model Checking. 18. FASE 2015. London, UK. April 11-18, 2015
Sharygina N., Alberti F., Ghilardi S. (2015) A New Acceleration-Based Combination Framework for Array Properties. 10. FroCos 2015. Wroclaw, Poland. September 21-24, 2015
Sharygina N., Hyvärinen A., Alt L. (2015) Flexible Interpolation for Efficient Model Checking. MEMICS 2015. Telč, Czech Republic. October 23-25, 2015
Sharygina N., Hyvärinen A., Marescotti M. (2015) Search-Space Partitioning for Parallelizing SMT Solvers. 18th SAT 2015. Austin, TX, USA. September 24-27, 2015
Sharygina N., Alt L., Fedyukovich G., Hyvärinen A. (2015) A Proof-Sensitive Approach for Small Propositional Interpolants. 7. VSTTE 2015. San Francisco, CA, USA. July 18-19, 2015
Sharygina N., Alberti F., Ghilardi S. (2014) Booster: An Acceleration-Based Verification Framework for Array Programs. 12th ATVA 2014. Sydney, NSW, Australia. November 3-7, 2014
Sharygina N., Jancík P., Rollini S. F., Kofron J. (2014) On interpolants and variable assignments. 14th FMCAD 2014. Lausanne, Switzerland. October 21-24, 2014
Sharygina N., Pastore F., Mariani L., Hyvärinen A., Fedyukovich G., Sehestedt S., Ali M. (2014) Verification-aided regression testing. ISSTA 2014. San Jose, CA. July 21 - 26, 2014
Sery O., Sharygina N., Denaro G., Ling M., Fedyukovich G., Hyvrinen A. E. J., Mariani L., Chockler H., Muhammad A., Oriol M., Rajan A., Tautschnig M. (2013) PINCETTE - Validating Changes and Upgrades in Networked Software. CSMR
Fedyukovich G., Sery O., Sharygina N. (2013) eVolCheck: Incremental Upgrade Checker for C. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer
Alberti F., Bruttomesso R., Ranise S., Sharygina N. (2012) SAFARI: SMT-based Abstraction For Arrays with Interpolants. 24th International Conference on Computer Aided Verification (CAV). Springer. Berkeley, California, USA
Alberti F., Bruttomesso R., Ranise S., Sharygina N. (2012) Lazy Abstraction with Interpolants for Arrays. 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). Springer. Méda, Venezuela
Sery O., Fedyukovich G., Sharygina N. (2012) FunFrog: Bounded Model Checking with Interpolation-based Function Summarization. Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA). Thiruvananthapuram, India
Sery O., Fedyukovich G., Sharygina N. (2012) Incremental Upgrade Checking by Means of Interpolation-based Function Summaries. Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD). Cambridge, UK
Rollini S. F., Sery O., Sharygina N. (2012) Leveraging Interpolant Strength in Model Checking. 24th International Conference on Computer Aided Verification (CAV). Springer. Berkeley, California, USA
Tsitovich A., Sharygina N., Wintersteiger C. M., Kröning D. (2011) Loop Summarization and Termination Analysis. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer. Saarbrü Germany
Sery O., Fedyukovich G., Sharygina N. (2011) Interpolation-based Function Summaries in Bounded Model Checking. Haifa Verification Conference (HVC). Springer. Haifa, Israel
Kröning D., Sharygina N., Tsitovich A., Wintersteiger C. M. (2010) Termination Analysis with Compositional Transition Invariants. International Conference on Computer-Aided Verification (CAV). Springer. Edinburgh, UK
Rollini S. F., Bruttomesso R., Sharygina N. (2010) An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference (HVC). Springer. Haifa, Israel
Bruttomesso R., Rollini S. F., Sharygina N., Tsitovich A. (2010) Flexible Interpolation with Local Proof Transformations. International Conference of Computer Aided Design (ICCAD). IEEE Computer Society. San Jose, USA
Bruttomesso R., Pek E., Sharygina N. (2010) A Flexible Schema for Generating Explanations in Lazy Theory Propagation. International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE Computer Society. Grenoble, France
Bruttomesso R., Pek E., Sharygina N., Tsitovich A. (2010) The OpenSMT Solver. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer. Paphos, Cyprus
Kröning D., Sharygina N., Tonetta S., Tsitovich A., Wintersteiger C. M. (2009) Loopfrog: A Static Analyzer for ANSI-C Programs. The 24th IEEE/ACM International Conference on Automated Software Engineering. IEEE Computer Society. Auckland, New Zealand
Bruttomesso R., Sharygina N. (2009) A Scalable Decision Procedure for Fixed-Width Bit-Vectors. International Conference of Computer Aided Design (ICCAD). ACM. San Jose (CA)
Sharygina N., Tonetta S., Tsitovich A. (2009) The Synergy of Precise and Fast Abstractions for Program Verification. 24th Annual ACM Symposium on Applied Computing (SAC). ACM. Honolulu, USA
Blanc N., Kröning D., Sharygina N. (2008) Scoot: A Tool for the Analysis of SystemC Models. TACAS
Kröning D., Sharygina N., Tonetta S., Tsitovich A., Wintersteiger C. M. (2008) Loop Summarization using Abstract Transformers. 6th International Symposium on Automated Technology for Verification and Analysis (ATVA). Springer. Seoul, South Korea
Jain H., Kröning D., Sharygina N., Clarke E. M. (2007) VCEGAR: Verilog CounterExample Guided Abstraction Refinement.. Lecture Notes in Computer Science. Springer
Aldrich J., Leavens G. T., Barnett M., Sharygina N., Giannakopoulou D. (2007) Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE (Companion)
Kröning D., Sharygina N. (2007) Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs.. DATE. ACM
Braghin C., Sharygina N., Barone-Adesi K. (2007) Automated Verification of Security Policies in Mobile Code.. Integrated Formal Methods (IFM). Springer