Natasha Sharygina

Orcid: 0000-0002-8872-4913

Affiliations:
  • University of Lugano, Switzerland


According to our database1, Natasha Sharygina authored at least 126 papers between 2001 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Reachability Analysis for Multiloop Programs Using Transition Power Abstraction.
Proceedings of the Formal Methods - 26th International Symposium, 2024

SolTG: A CHC-Based Solidity Test Case Generator.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023
A Solicitous Approach to Smart Contract Verification.
ACM Trans. Priv. Secur., May, 2023

Picky CDCL: SMT-Solving with Flexible Literal Selection.
Proceedings of the Verified Software. Theories, Tools and Experiments, 2023

Symbolic Model Checking for TLA+ Made Faster.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

CHC Model Validation with Proof Guarantees.
Proceedings of the iFM 2023 - 18th International Conference, 2023

The Golem Horn Solver.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022
Using linear algebra in decomposition of Farkas interpolants.
Int. J. Softw. Tools Technol. Transf., 2022

SMT-based verification of program changes through summary repair.
Formal Methods Syst. Des., 2022

Transition Power Abstractions for Deep Counterexample Detection.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Split Transition Power Abstraction for Unbounded Safety.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

SolCMC: Solidity Compiler's Model Checker.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021
Lookahead in Partitioning SMT.
Proceedings of the Formal Methods in Computer Aided Design, 2021

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions.
Proceedings of the 58th ACM/IEEE Design Automation Conference, 2021

2020
A Cooperative Parallelization Approach for Property-Directed k-Induction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Farkas-Based Tree Interpolation.
Proceedings of the Static Analysis - 27th International Symposium, 2020

Accurate Smart Contract Verification Through Direct Modelling.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Applications, 2020

Incremental Verification by SMT-based Summary Repair.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019
Exploiting partial variable assignment in interpolation-based model checking.
Formal Methods Syst. Des., 2019

Decomposing Farkas Interpolants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Lattice-based SMT for program verification.
Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2019

2018
Modeling for Verification.
Proceedings of the Handbook of Model Checking., 2018

Lattice-Based Refinement in Bounded Model Checking.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

SMTS: Distributed, Visualized Constraint Solving.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Lookahead-Based SMT Solving.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Function Summarization Modulo Theories.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Computing Exact Worst-Case Gas Consumption for Smart Contracts.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

2017
Flexible SAT-based framework for incremental bounded upgrade checking.
Int. J. Softw. Tools Technol. Transf., 2017

A Framework for the Verification of Parameterized Infinite-state Systems.
Fundam. Informaticae, 2017

HiFrog: SMT-based Function Summarization for Software Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Visualising SMT-Based Parallel Constraint Solving.
Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Theory Refinement for Program Verification.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

LRA Interpolants from No Man's Land.
Proceedings of the Hardware and Software: Verification and Testing, 2017

Designing parallel PDR.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Duality-based interpolation for quantifier-free equalities and uninterpreted functions.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016
OpenSMT2: An SMT Solver for Multi-core and Cloud Computing.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

PVAIR: Partial Variable Assignment InterpolatoR.
Proceedings of the Fundamental Approaches to Software Engineering, 2016

Property Directed Equivalence via Abstract Simulation.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Clause Sharing and Partitioning for Cloud-Based SMT Solving.
Proceedings of the Automated Technology for Verification and Analysis, 2016

2015
Decision Procedures for Flat Array Properties.
J. Autom. Reason., 2015

A Proof-Sensitive Approach for Small Propositional Interpolants.
Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Search-Space Partitioning for Parallelizing SMT Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Flexible Interpolation for Efficient Model Checking.
Proceedings of the Mathematical and Engineering Methods in Computer Science, 2015

Automated Discovery of Simulation Between Programs.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A New Acceleration-Based Combination Framework for Array Properties.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Symbolic Detection of Assertion Dependencies for Bounded Model Checking.
Proceedings of the Fundamental Approaches to Software Engineering, 2015

Incremental Upgrade Checking.
Proceedings of the Validation of Evolving Software, 2015

Function Summarization-Based Bounded Model Checking.
Proceedings of the Validation of Evolving Software, 2015

Optimizing Function Summaries Through Interpolation.
Proceedings of the Validation of Evolving Software, 2015

Regression Checking of Changes in C Software.
Proceedings of the Validation of Evolving Software, 2015

Complementarities Among the Technologies Presented in the Book.
Proceedings of the Validation of Evolving Software, 2015

Challenges of Existing Technology.
Proceedings of the Validation of Evolving Software, 2015

Introduction.
Proceedings of the Validation of Evolving Software, 2015

2014
Resolution proof transformation for compression and interpolation.
Formal Methods Syst. Des., 2014

An extension of lazy abstraction with interpolation for programs with arrays.
Formal Methods Syst. Des., 2014

Monotonic Abstraction Techniques: from Parametric to Software Model Checking.
Proceedings of the Proceedings First Workshop on Logics and Model-checking for Self-* Systems, 2014

Verige: verification with invariant generation engine.
Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection.
Proceedings of the Formal Methods: Foundations and Applications - 17th Brazilian Symposium, 2014

Incremental Verification of Compiler Optimizations.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Verification-aided regression testing.
Proceedings of the International Symposium on Software Testing and Analysis, 2014

On interpolants and variable assignments.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Booster: An Acceleration-Based Verification Framework for Array Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
Loop summarization using state and transition invariants.
Formal Methods Syst. Des., 2013

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
CoRR, 2013

eVolCheck: Incremental Upgrade Checker for C.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Using cross-entropy for satisfiability.
Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013

A Parametric Interpolation Framework for First-Order Theories.
Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Acceleration-based safety decision procedure for programs with arrays.
Proceedings of the LPAR 2013, 2013

Definability of Accelerated Relations in a Theory of Arrays and Its Applications.
Proceedings of the Frontiers of Combining Systems, 2013

Interpolation-based model checking for efficient incremental analysis of software.
Proceedings of the 16th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, 2013

PINCETTE - Validating Changes and Upgrades in Networked Software.
Proceedings of the 17th European Conference on Software Maintenance and Reengineering, 2013

Interpolation Properties and SAT-Based Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
An abstraction refinement approach combining precise and approximated techniques.
Int. J. Softw. Tools Technol. Transf., 2012

Propositional Interpolation Systems for Model Checking
CoRR, 2012

Lazy Abstraction with Interpolants for Arrays.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Incremental upgrade checking by means of interpolation-based function summaries.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Leveraging Interpolant Strength in Model Checking.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

SAFARI: SMT-Based Abstraction for Arrays with Interpolants.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Reachability Modulo Theory Library.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization.
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
A model checking-based approach for security policy verification of mobile systems.
Formal Aspects Comput., 2011

Loop Summarization and Termination Analysis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Interpolation-Based Function Summaries in Bounded Model Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2011

Function Summaries in Software Upgrade Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2011

2010
The OpenSMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

A flexible schema for generating explanations in lazy theory propagation.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Flexible interpolation with local proof transformations.
Proceedings of the 2010 International Conference on Computer-Aided Design, 2010

An Efficient and Flexible Approach to Resolution Proof Reduction.
Proceedings of the Hardware and Software: Verification and Testing, 2010

Termination Analysis with Compositional Transition Invariants.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Loopfrog - loop summarization for static analysis.
Proceedings of the Second International Workshop on Invariant Generation, 2010

2009
An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk.
Proceedings of the SAVCBS'09, 2009

The synergy of precise and fast abstractions for program verification.
Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Loopfrog: A Static Analyzer for ANSI-C Programs.
Proceedings of the ASE 2009, 2009

A scalable decision procedure for fixed-width bit-vectors.
Proceedings of the 2009 International Conference on Computer-Aided Design, 2009

2008
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Verification of evolving software via component substitutability analysis.
Formal Methods Syst. Des., 2008

Scoot: A Tool for the Analysis of SystemC Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Loop Summarization Using Abstract Transformers.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
Verification of Boolean programs with unbounded thread creation.
Theor. Comput. Sci., 2007

VCEGAR: Verilog CounterExample Guided Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Model Checking with Abstraction for Web Services.
Proceedings of the Test and Analysis of Web Services, 2007

Specification and verification of component-based systems 2007.
Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Automated Verification of Security Policies in Mobile Code.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

2006
Approximating Predicate Images for Bit-Vector Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Over-Approximating Boolean Programs with Unbounded Thread Creation.
Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

2005
Concurrent software verification with states, events, and deadlocks.
Formal Aspects Comput., 2005

SATABS: SAT-Based Predicate Abstraction for ANSI-C.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Symbolic Model Checking for Asynchronous Boolean Programs.
Proceedings of the Model Checking Software, 2005

Formal verification of SystemC by automatic hardware/software partitioning.
Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

State/Event Software Verification for Branching-Time Specifications.
Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Program Compatibility Approaches.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Dynamic Component Substitutability Analysis.
Proceedings of the FM 2005: Formal Methods, 2005

Word level predicate abstraction and refinement for verifying RTL verilog.
Proceedings of the 42nd Design Automation Conference, 2005

Cogent: Accurate Theorem Proving for Program Verification.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The ComFoRT Reasoning Framework.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Lessons Learned from Model Checking a NASA Robot Controller.
Formal Methods Syst. Des., 2004

Guest Editorial.
Formal Methods Syst. Des., 2004

Predicate Abstraction of ANSI-C Programs Using SAT.
Formal Methods Syst. Des., 2004

Automated, compositional and iterative deadlock detection.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Accurate Theorem Proving for Program Verification.
Proceedings of the Leveraging Applications of Formal Methods, 2004

State/Event-Based Software Model Checking.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

2003
Model Checking Software via Abstraction of Loop Transitions.
Proceedings of the Fundamental Approaches to Software Engineering, 2003

2001
A Combined Testing and Verification Approach for Software Reliability.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

A Formal Object-Oriented Analysis for Software Reliability: Design for Verification.
Proceedings of the Fundamental Approaches to Software Engineering, 2001


  Loading...