Natasha Sharygina
http://usi.to/fqf
Pubblicazioni
Pubblicazioni principali (1)
- Bruttomesso R., Pek E., Sharygina N., Tsitovich A. (2010) The OpenSMT Solver
Articolo pubblicato in rivista scientifica (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
Libro (1)
- Sharygina N., Kröning D. (2007) Model Checking with Abstraction for Web Services.. Springer. Test and Analysis of Web Services
Atti di conferenza (1)
- Fedyukovich G., Sery O., Sharygina N. (2011) Function Summaries in Software Upgrade Checking. Springer. Haifa, Israel
Contributo in atti di convegno (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
Rapporto tecnico (3)
- Fedyukovich G., Sharygina N., Gurfinkel A. (2013) Automated Discovery of Simulation Between Programs
- Alberti F., Sharygina N. (2013) Decision Procedures for Flat Array Properties
- Alberti F., Sharygina N. (2012) Tackling divergence: abstraction and acceleration in array programs