Natasha Sharygina

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 44

Top Venues

FMCAD

LPAR

Formal Methods Syst. Des.

VSTTE

Publications

Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt, Natasha Sharygina
SolTG: A CHC-Based Solidity Test Case Generator. CAV (1) (2024)
Martin Blicha, Konstantin Britikov, Natasha Sharygina
The Golem Horn Solver. CAV (2) (2023)
Konstantin Britikov, Antti E. J. Hyvärinen, Natasha Sharygina
Picky CDCL: SMT-Solving with Flexible Literal Selection. VSTTE (2023)
Rodrigo Otoni, Martin Blicha, Patrick Eugster, Natasha Sharygina
CHC Model Validation with Proof Guarantees. iFM (2023)
Rodrigo Otoni, Matteo Marescotti, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
A Solicitous Approach to Smart Contract Verification. ACM Trans. Priv. Secur. 26 (2) (2023)
Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina
Symbolic Model Checking for TLA+ Made Faster. TACAS (1) (2023)
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
Using linear algebra in decomposition of Farkas interpolants. Int. J. Softw. Tools Technol. Transf. 24 (1) (2022)
Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Split Transition Power Abstraction for Unbounded Safety. FMCAD (2022)
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
SMT-based verification of program changes through summary repair. Formal Methods Syst. Des. 60 (3) (2022)
Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, Natasha Sharygina
SolCMC: Solidity Compiler's Model Checker. CAV (1) (2022)
Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Transition Power Abstractions for Deep Counterexample Detection. TACAS (1) (2022)
Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. DAC (2021)
Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
Lookahead in Partitioning SMT. FMCAD (2021)
Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
Accurate Smart Contract Verification Through Direct Modelling. ISoLA (3) (2020)
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
Incremental Verification by SMT-based Summary Repair. FMCAD (2020)
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
Farkas-Based Tree Interpolation. SAS (2020)
Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
A Cooperative Parallelization Approach for Property-Directed k-Induction. VMCAI (2020)
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
Decomposing Farkas Interpolants. TACAS (1) (2019)
Karine Even-Mendoza, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina
Lattice-based SMT for program verification. MEMOCODE (2019)
Pavel Jancík, Jan Kofron, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Exploiting partial variable assignment in interpolation-based model checking. Formal Methods Syst. Des. 55 (1) (2019)
Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
SMTS: Distributed, Visualized Constraint Solving. LPAR (2018)
Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler
Function Summarization Modulo Theories. LPAR (2018)
Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi, Natasha Sharygina
Computing Exact Worst-Case Gas Consumption for Smart Contracts. ISoLA (4) (2018)
Antti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina
Lookahead-Based SMT Solving. LPAR (2018)
Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina
Lattice-Based Refinement in Bounded Model Checking. VSTTE (2018)
Leonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina
Duality-based interpolation for quantifier-free equalities and uninterpreted functions. FMCAD (2017)
Leonardo Alt, Antti E. J. Hyvärinen, Natasha Sharygina
LRA Interpolants from No Man's Land. Haifa Verification Conference (2017)
Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
HiFrog: SMT-based Function Summarization for Software Verification. TACAS (2) (2017)
Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina
Designing parallel PDR. FMCAD (2017)
Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
Flexible SAT-based framework for incremental bounded upgrade checking. Int. J. Softw. Tools Technol. Transf. 19 (5) (2017)
Jelena Budakovic, Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
Visualising SMT-Based Parallel Constraint Solving. SMT (2017)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Informaticae 150 (1) (2017)
Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina
Theory Refinement for Program Verification. SAT (2017)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Property Directed Equivalence via Abstract Simulation. CAV (2) (2016)
Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
Clause Sharing and Partitioning for Cloud-Based SMT Solving. ATVA (2016)
Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina
OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. SAT (2016)
Pavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
PVAIR: Partial Variable Assignment InterpolatoR. FASE (2016)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. J. Autom. Reason. 54 (4) (2015)
Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, Natasha Sharygina
Symbolic Detection of Assertion Dependencies for Bounded Model Checking. FASE (2015)
Antti E. J. Hyvärinen, Leonardo Alt, Natasha Sharygina
Flexible Interpolation for Efficient Model Checking. MEMICS (2015)
Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
Search-Space Partitioning for Parallelizing SMT Solvers. SAT (2015)
Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
A Proof-Sensitive Approach for Small Propositional Interpolants. VSTTE (2015)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A New Acceleration-Based Combination Framework for Array Properties. FroCos (2015)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Automated Discovery of Simulation Between Programs. LPAR (2015)
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45 (1) (2014)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Incremental Verification of Compiler Optimizations. NASA Formal Methods (2014)
Fabrizio Pastore, Leonardo Mariani, Antti Eero Johannes Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, Ali Muhammad
Verification-aided regression testing. ISSTA (2014)
Grigory Fedyukovich, Natasha Sharygina
Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection. SBMF (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
A Framework for the Verification of Parameterized Infinite-State Systems. CILC (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Monotonic Abstraction Techniques: from Parametric to Software Model Checking. MOD* (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. TACAS (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Decision Procedures for Flat Array Properties. SMT (2014)
Pavel Jancík, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina
On interpolants and variable assignments. FMCAD (2014)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45 (1) (2014)
Nicolas Latorre, Francesco Alberti, Natasha Sharygina
Verige: verification with invariant generation engine. SPIN (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Booster: An Acceleration-Based Verification Framework for Array Programs. ATVA (2014)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Acceleration-based safety decision procedure for programs with arrays. LPAR (short papers) (2013)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Definability of Accelerated Relations in a Theory of Arrays and Its Applications. FroCos (2013)
Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
Interpolation Properties and SAT-Based Model Checking. ATVA (2013)
Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
eVolCheck: Incremental Upgrade Checker for C. TACAS (2013)
Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina
PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. LPAR (2013)
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
Loop summarization using state and transition invariants. Formal Methods Syst. Des. 42 (3) (2013)
Laura Kovács, Simone Fulvio Rollini, Natasha Sharygina
A Parametric Interpolation Framework for First-Order Theories. MICAI (1) (2013)
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs CoRR (2013)
Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Interpolation-based model checking for efficient incremental analysis of software. DDECS (2013)
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
Resolution Proof Transformation for Compression and Interpolation. CoRR (2013)
Hana Chockler, Giovanni Denaro, Meijia Ling, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Leonardo Mariani, Ali Muhammad, Manuel Oriol, Ajitha Rajan, Ondrej Sery, Natasha Sharygina, Michael Tautschnig
PINCETTE - Validating Changes and Upgrades in Networked Software. CSMR (2013)
Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina
Using cross-entropy for satisfiability. SAC (2013)
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. ATVA (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Lazy Abstraction with Interpolants for Arrays. LPAR (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Reachability Modulo Theory Library. SMT@IJCAR (2012)
Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina
Leveraging Interpolant Strength in Model Checking. CAV (2012)
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
Incremental upgrade checking by means of interpolation-based function summaries. FMCAD (2012)
Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
An abstraction refinement approach combining precise and approximated techniques. Int. J. Softw. Tools Technol. Transf. 14 (1) (2012)
Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
Propositional Interpolation Systems for Model Checking CoRR (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV (2012)
Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi
A model checking-based approach for security policy verification of mobile systems. Formal Aspects Comput. 23 (5) (2011)
Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
Function Summaries in Software Upgrade Checking. Haifa Verification Conference (2011)
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
Interpolation-Based Function Summaries in Bounded Model Checking. Haifa Verification Conference (2011)
Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening
Loop Summarization and Termination Analysis. TACAS (2011)
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich
The OpenSMT Solver. TACAS (2010)
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
A flexible schema for generating explanations in lazy theory propagation. MEMOCODE (2010)
Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich
Flexible interpolation with local proof transformations. ICCAD (2010)
Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
Termination Analysis with Compositional Transition Invariants. CAV (2010)
Simone Rollini, Roberto Bruttomesso, Natasha Sharygina
An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference (2010)
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
Loopfrog - loop summarization for static analysis. WING@ETAPS/IJCAR (2010)
Roberto Bruttomesso, Natasha Sharygina
A scalable decision procedure for fixed-width bit-vectors. ICCAD (2009)
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
Loopfrog: A Static Analyzer for ANSI-C Programs. ASE (2009)
Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk. SAVCBS (2009)
Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
The synergy of precise and fast abstractions for program verification. SAC (2009)
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
Loop Summarization Using Abstract Transformers. ATVA (2008)
Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
Verification of evolving software via component substitutability analysis. Formal Methods Syst. Des. 32 (3) (2008)
Nicolas Blanc, Daniel Kroening, Natasha Sharygina
Scoot: A Tool for the Analysis of SystemC Models. TACAS (2008)
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27 (2) (2008)
Gary T. Leavens, Dimitra Giannakopoulou, Jonathan Aldrich, Michael Barnett, Natasha Sharygina
Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE (Companion) (2007)
Byron Cook, Daniel Kroening, Natasha Sharygina
Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. 388 (1-3) (2007)
Daniel Kroening, Natasha Sharygina
Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. DATE (2007)
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS (2007)
Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi
Automated Verification of Security Policies in Mobile Code. IFM (2007)
Jonathan Aldrich, Michael Barnett, Dimitra Giannakopoulou, Gary T. Leavens, Natasha Sharygina
Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE (2007)

Natasha Sharygina.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Natasha Sharygina