A Formal Object-Oriented Analysis for Software Reliability: Design for Verification. - Natasha Sharygina; James C. Browne; Robert P. Kurshan (FASE, 2001)

A Combined Testing and Verification Approach for Software Reliability. - Natasha Sharygina; Doron A. Peled (FME, 2001)

Model Checking Software via Abstraction of Loop Transitions. - Natasha Sharygina; James C. Browne (FASE, 2003)

State/Event-Based Software Model Checking. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina; Nishant Sinha 001 (IFM, 2004)

Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (ISoLA, 2004)

Automated, compositional and iterative deadlock detection. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina (MEMOCODE, 2004)

Predicate Abstraction of ANSI-C Programs Using SAT. - Edmund M. Clarke; Daniel Kroening; Natasha Sharygina; Karen Yorav (Formal Methods Syst. Des., 2004)

Guest Editorial. - Natasha Sharygina (Formal Methods Syst. Des., 2004)

Lessons Learned from Model Checking a NASA Robot Controller. - Natasha Sharygina; James C. Browne; Fei Xie; Robert P. Kurshan; Vladimir Levin (Formal Methods Syst. Des., 2004)

The ComFoRT Reasoning Framework. - Sagar Chaki; James Ivers; Natasha Sharygina; Kurt C. Wallnau (CAV, 2005)

Cogent: Accurate Theorem Proving for Program Verification. - Byron Cook; Daniel Kroening; Natasha Sharygina (CAV, 2005)

Word level predicate abstraction and refinement for verifying RTL verilog. - Himanshu Jain; Daniel Kroening; Natasha Sharygina; Edmund M. Clarke (DAC, 2005)

Dynamic Component Substitutability Analysis. - Natasha Sharygina; Sagar Chaki; Edmund M. Clarke; Nishant Sinha 001 (FM, 2005)

Program Compatibility Approaches. - Edmund M. Clarke; Natasha Sharygina; Nishant Sinha 001 (FMCO, 2005)

State/Event Software Verification for Branching-Time Specifications. - Sagar Chaki; Edmund M. Clarke; Orna Grumberg; Joël Ouaknine; Natasha Sharygina; Tayssir Touili; Helmut Veith (IFM, 2005)

Formal verification of SystemC by automatic hardware/software partitioning. - Daniel Kroening; Natasha Sharygina (MEMOCODE, 2005)

Symbolic Model Checking for Asynchronous Boolean Programs. - Byron Cook; Daniel Kroening; Natasha Sharygina (SPIN, 2005)

SATABS: SAT-Based Predicate Abstraction for ANSI-C. - Edmund M. Clarke; Daniel Kroening; Natasha Sharygina; Karen Yorav (TACAS, 2005)

Concurrent software verification with states, events, and deadlocks. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina; Nishant Sinha 001 (Formal Aspects Comput., 2005)

Over-Approximating Boolean Programs with Unbounded Thread Creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (FMCAD, 2006)

Approximating Predicate Images for Bit-Vector Logic. - Daniel Kroening; Natasha Sharygina (TACAS, 2006)

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. - Daniel Kroening; Natasha Sharygina (DATE, 2007)

Automated Verification of Security Policies in Mobile Code. - Chiara Braghin; Natasha Sharygina; Katerina Barone-Adesi (IFM, 2007)

Specification and verification of component-based systems 2007. - Jonathan Aldrich; Michael Barnett 001; Dimitra Giannakopoulou; Gary T. Leavens; Natasha Sharygina (ESEC/SIGSOFT FSE, 2007)

Model Checking with Abstraction for Web Services. - Natasha Sharygina; Daniel Kröning (Test and Analysis of Web Services, 2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement. - Himanshu Jain; Daniel Kroening; Natasha Sharygina; Edmund M. Clarke (TACAS, 2007)

Verification of Boolean programs with unbounded thread creation. - Byron Cook; Daniel Kroening; Natasha Sharygina (Theor. Comput. Sci., 2007)

Loop Summarization Using Abstract Transformers. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ATVA, 2008)

Scoot: A Tool for the Analysis of SystemC Models. - Nicolas Blanc; Daniel Kroening; Natasha Sharygina (TACAS, 2008)

Verification of evolving software via component substitutability analysis. - Sagar Chaki; Edmund M. Clarke; Natasha Sharygina; Nishant Sinha 001 (Formal Methods Syst. Des., 2008)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. - Himanshu Jain; Daniel Kroening; Natasha Sharygina; Edmund M. Clarke (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

A scalable decision procedure for fixed-width bit-vectors. - Roberto Bruttomesso; Natasha Sharygina (ICCAD, 2009)

Loopfrog: A Static Analyzer for ANSI-C Programs. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ASE, 2009)

The synergy of precise and fast abstractions for program verification. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (SAC, 2009)

An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (SAVCBS, 2009)

Loopfrog - loop summarization for static analysis. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (WING@ETAPS/IJCAR, 2010)

Termination Analysis with Compositional Transition Invariants. - Daniel Kroening; Natasha Sharygina; Aliaksei Tsitovich; Christoph M. Wintersteiger (CAV, 2010)

An Efficient and Flexible Approach to Resolution Proof Reduction. - Simone Rollini; Roberto Bruttomesso; Natasha Sharygina (Haifa Verification Conference, 2010)

Flexible interpolation with local proof transformations. - Roberto Bruttomesso; Simone Rollini; Natasha Sharygina; Aliaksei Tsitovich (ICCAD, 2010)

A flexible schema for generating explanations in lazy theory propagation. - Roberto Bruttomesso; Edgar Pek; Natasha Sharygina (MEMOCODE, 2010)

The OpenSMT Solver. - Roberto Bruttomesso; Edgar Pek; Natasha Sharygina; Aliaksei Tsitovich (TACAS, 2010)

Function Summaries in Software Upgrade Checking. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (Haifa Verification Conference, 2011)

Interpolation-Based Function Summaries in Bounded Model Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Haifa Verification Conference, 2011)

Loop Summarization and Termination Analysis. - Aliaksei Tsitovich; Natasha Sharygina; Christoph M. Wintersteiger; Daniel Kroening (TACAS, 2011)

A model checking-based approach for security policy verification of mobile systems. - Chiara Braghin; Natasha Sharygina; Katerina Barone-Adesi (Formal Aspects Comput., 2011)

FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (ATVA, 2012)

Reachability Modulo Theory Library. - Francesco Alberti; Roberto Bruttomesso; Silvio Ghilardi; Silvio Ranise; Natasha Sharygina (SMT@IJCAR, 2012)

SAFARI: SMT-Based Abstraction for Arrays with Interpolants. - Francesco Alberti; Roberto Bruttomesso; Silvio Ghilardi; Silvio Ranise; Natasha Sharygina (CAV, 2012)

Leveraging Interpolant Strength in Model Checking. - Simone Fulvio Rollini; Ondrej Sery; Natasha Sharygina (CAV, 2012)

Incremental upgrade checking by means of interpolation-based function summaries. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (FMCAD, 2012)

Lazy Abstraction with Interpolants for Arrays. - Francesco Alberti; Roberto Bruttomesso; Silvio Ghilardi; Silvio Ranise; Natasha Sharygina (LPAR, 2012)

Propositional Interpolation Systems for Model Checking - Arie Gurfinkel; Simone Fulvio Rollini; Natasha Sharygina (CoRR, 2012)

An abstraction refinement approach combining precise and approximated techniques. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (Int. J. Softw. Tools Technol. Transf., 2012)

Interpolation Properties and SAT-Based Model Checking. - Arie Gurfinkel; Simone Fulvio Rollini; Natasha Sharygina (ATVA, 2013)

PINCETTE - Validating Changes and Upgrades in Networked Software. - 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 (CSMR, 2013)

Interpolation-based model checking for efficient incremental analysis of software. - Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (DDECS, 2013)

Definability of Accelerated Relations in a Theory of Arrays and Its Applications. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (FroCos, 2013)

Acceleration-based safety decision procedure for programs with arrays. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (LPAR (short papers), 2013)

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. - Simone Fulvio Rollini; Leonardo Alt; Grigory Fedyukovich; Antti Eero Johannes Hyvärinen; Natasha Sharygina (LPAR, 2013)

A Parametric Interpolation Framework for First-Order Theories. - Laura Kovács; Simone Fulvio Rollini; Natasha Sharygina (MICAI (1), 2013)

Using cross-entropy for satisfiability. - Hana Chockler; Alexander Ivrii; Arie Matsliah; Simone Fulvio Rollini; Natasha Sharygina (SAC, 2013)

eVolCheck: Incremental Upgrade Checker for C. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (TACAS, 2013)

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (CoRR, 2013)

Loop summarization using state and transition invariants. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Booster: An Acceleration-Based Verification Framework for Array Programs. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (ATVA, 2014)

On interpolants and variable assignments. - Pavel Jancík; Jan Kofron; Simone Fulvio Rollini; Natasha Sharygina (FMCAD, 2014)

Verification-aided regression testing. - Fabrizio Pastore; Leonardo Mariani; Antti Eero Johannes Hyvärinen; Grigory Fedyukovich; Natasha Sharygina; Stephan Sehestedt; Ali Muhammad (ISSTA, 2014)

Incremental Verification of Compiler Optimizations. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (NASA Formal Methods, 2014)

Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection. - Grigory Fedyukovich; Natasha Sharygina (SBMF, 2014)

Verige: verification with invariant generation engine. - Nicolas Latorre; Francesco Alberti; Natasha Sharygina (SPIN, 2014)

Monotonic Abstraction Techniques: from Parametric to Software Model Checking. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (MOD*, 2014)

An extension of lazy abstraction with interpolation for programs with arrays. - Francesco Alberti; Roberto Bruttomesso; Silvio Ghilardi; Silvio Ranise; Natasha Sharygina (Formal Methods Syst. Des., 2014)

Resolution proof transformation for compression and interpolation. - Simone Fulvio Rollini; Roberto Bruttomesso; Natasha Sharygina; Aliaksei Tsitovich (Formal Methods Syst. Des., 2014)

Introduction. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Challenges of Existing Technology. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Complementarities Among the Technologies Presented in the Book. - Hana Chockler; Daniel Kroening; Leonardo Mariani; Natasha Sharygina (Validation of Evolving Software, 2015)

Regression Checking of Changes in C Software. - Fabrizio Pastore; Leonardo Mariani; Antti Eero Johannes Hyvärinen; Grigory Fedyukovich; Natasha Sharygina; Stephan Sehestedt; Ali Muhammad (Validation of Evolving Software, 2015)

Optimizing Function Summaries Through Interpolation. - Simone Fulvio Rollini; Leonardo Alt; Grigory Fedyukovich; Antti Eero Johannes Hyvärinen; Natasha Sharygina (Validation of Evolving Software, 2015)

Function Summarization-Based Bounded Model Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Validation of Evolving Software, 2015)

Incremental Upgrade Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Validation of Evolving Software, 2015)

Symbolic Detection of Assertion Dependencies for Bounded Model Checking. - Grigory Fedyukovich; Andrea Callia D'Iddio; Antti E. J. Hyvärinen; Natasha Sharygina (FASE, 2015)

A New Acceleration-Based Combination Framework for Array Properties. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (FroCos, 2015)

Automated Discovery of Simulation Between Programs. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (LPAR, 2015)

Flexible Interpolation for Efficient Model Checking. - Antti E. J. Hyvärinen; Leonardo Alt; Natasha Sharygina (MEMICS, 2015)

Search-Space Partitioning for Parallelizing SMT Solvers. - Antti E. J. Hyvärinen; Matteo Marescotti; Natasha Sharygina (SAT, 2015)

A Proof-Sensitive Approach for Small Propositional Interpolants. - Leonardo Alt; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (VSTTE, 2015)

Decision Procedures for Flat Array Properties. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (J. Autom. Reason., 2015)

Clause Sharing and Partitioning for Cloud-Based SMT Solving. - Matteo Marescotti; Antti E. J. Hyvärinen; Natasha Sharygina (ATVA, 2016)

Property Directed Equivalence via Abstract Simulation. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (CAV (2), 2016)

PVAIR: Partial Variable Assignment InterpolatoR. - Pavel Jancík; Leonardo Alt; Grigory Fedyukovich; Antti E. J. Hyvärinen; Jan Kofron; Natasha Sharygina (FASE, 2016)

OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. - Antti E. J. Hyvärinen; Matteo Marescotti; Leonardo Alt; Natasha Sharygina (SAT, 2016)

Duality-based interpolation for quantifier-free equalities and uninterpreted functions. - Leonardo Alt; Antti Eero Johannes Hyvärinen; Sepideh Asadi; Natasha Sharygina (FMCAD, 2017)

Designing parallel PDR. - Matteo Marescotti; Arie Gurfinkel; Antti Eero Johannes Hyvärinen; Natasha Sharygina (FMCAD, 2017)

LRA Interpolants from No Man's Land. - Leonardo Alt; Antti E. J. Hyvärinen; Natasha Sharygina (Haifa Verification Conference, 2017)

Theory Refinement for Program Verification. - Antti E. J. Hyvärinen; Sepideh Asadi; Karine Even-Mendoza; Grigory Fedyukovich; Hana Chockler; Natasha Sharygina (SAT, 2017)

Visualising SMT-Based Parallel Constraint Solving. - Jelena Budakovic; Matteo Marescotti; Antti E. J. Hyvärinen; Natasha Sharygina (SMT, 2017)

HiFrog: SMT-based Function Summarization for Software Verification. - Leonardo Alt; Sepideh Asadi; Hana Chockler; Karine Even-Mendoza; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (TACAS (2), 2017)

A Framework for the Verification of Parameterized Infinite-state Systems. - Francesco Alberti; Silvio Ghilardi; Natasha Sharygina (Fundam. Informaticae, 2017)

Flexible SAT-based framework for incremental bounded upgrade checking. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (Int. J. Softw. Tools Technol. Transf., 2017)

Computing Exact Worst-Case Gas Consumption for Smart Contracts. - Matteo Marescotti; Martin Blicha; Antti E. J. Hyvärinen; Sepideh Asadi; Natasha Sharygina (ISoLA (4), 2018)

Function Summarization Modulo Theories. - Sepideh Asadi; Martin Blicha; Grigory Fedyukovich; Antti E. J. Hyvärinen; Karine Even-Mendoza; Natasha Sharygina; Hana Chockler (LPAR, 2018)

Lookahead-Based SMT Solving. - Antti E. J. Hyvärinen; Matteo Marescotti; Parvin Sadigova; Hana Chockler; Natasha Sharygina (LPAR, 2018)

SMTS: Distributed, Visualized Constraint Solving. - Matteo Marescotti; Antti E. J. Hyvärinen; Natasha Sharygina (LPAR, 2018)

Lattice-Based Refinement in Bounded Model Checking. - Karine Even-Mendoza; Sepideh Asadi; Antti E. J. Hyvärinen; Hana Chockler; Natasha Sharygina (VSTTE, 2018)

Modeling for Verification. - Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (Handbook of Model Checking, 2018)

Lattice-based SMT for program verification. - Karine Even-Mendoza; Antti E. J. Hyvärinen; Hana Chockler; Natasha Sharygina (MEMOCODE, 2019)

Decomposing Farkas Interpolants. - Martin Blicha; Antti E. J. Hyvärinen; Jan Kofron; Natasha Sharygina (TACAS (1), 2019)

Exploiting partial variable assignment in interpolation-based model checking. - Pavel Jancík; Jan Kofron; Leonardo Alt; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (Formal Methods Syst. Des., 2019)

Incremental Verification by SMT-based Summary Repair. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (FMCAD, 2020)

Accurate Smart Contract Verification Through Direct Modelling. - Matteo Marescotti; Rodrigo Otoni; Leonardo Alt; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (ISoLA (3), 2020)

Farkas-Based Tree Interpolation. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (SAS, 2020)

A Cooperative Parallelization Approach for Property-Directed k-Induction. - Martin Blicha; Antti E. J. Hyvärinen; Matteo Marescotti; Natasha Sharygina (VMCAI, 2020)

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (DAC, 2021)

Lookahead in Partitioning SMT. - Antti E. J. Hyvärinen; Matteo Marescotti; Natasha Sharygina (FMCAD, 2021)

SolCMC: Solidity Compiler's Model Checker. - Leonardo Alt; Martin Blicha; Antti E. J. Hyvärinen; Natasha Sharygina (CAV (1), 2022)

Split Transition Power Abstraction for Unbounded Safety. - Martin Blicha; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (FMCAD, 2022)

Transition Power Abstractions for Deep Counterexample Detection. - Martin Blicha; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (TACAS (1), 2022)

SMT-based verification of program changes through summary repair. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (Formal Methods Syst. Des., 2022)

Using linear algebra in decomposition of Farkas interpolants. - Martin Blicha; Antti E. J. Hyvärinen; Jan Kofron; Natasha Sharygina (Int. J. Softw. Tools Technol. Transf., 2022)

The Golem Horn Solver. - Martin Blicha; Konstantin Britikov; Natasha Sharygina (CAV (2), 2023)

CHC Model Validation with Proof Guarantees. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Natasha Sharygina (iFM, 2023)

Symbolic Model Checking for TLA+ Made Faster. - Rodrigo Otoni; Igor Konnov 001; Jure Kukovec; Patrick Eugster; Natasha Sharygina (TACAS (1), 2023)

Picky CDCL: SMT-Solving with Flexible Literal Selection. - Konstantin Britikov; Antti E. J. Hyvärinen; Natasha Sharygina (VSTTE, 2023)

A Solicitous Approach to Smart Contract Verification. - Rodrigo Otoni; Matteo Marescotti; Leonardo Alt; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (ACM Trans. Priv. Secur., 2023)

SolTG: A CHC-Based Solidity Test Case Generator. - Konstantin Britikov; Ilia Zlatkin; Grigory Fedyukovich; Leonardo Alt; Natasha Sharygina (CAV (1), 2024)

Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. - Konstantin Britikov; Martin Blicha; Natasha Sharygina; Grigory Fedyukovich (FM (1), 2024)

Space Explanations of Neural Network Classification. - Faezeh Labbaf; Tomás Kolárik; Martin Blicha; Grigory Fedyukovich; Michael Wand 002; Natasha Sharygina (CAV (3), 2025)

Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (TACAS (2), 2025)

Artifact for the paper Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (Zenodo, 2025)