Natasha Sharygina
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
82
Venues
21
Active years
2001–2026
Best venue rank
A*
Where they publish
Papers
82 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | PyCHC: A Framework for Certified Horn Solving and CHC-Based Design. | Anna Becchi, Martin Blicha, Rodrigo Otoni, Natasha Sharygina |
| 2026 | ESANN | Interpreting Logical Explanations of Classifying Neural Networks. | Fabrizio Leopardi, Faezeh Labbaf, Toms Kolrik, Michael Wand, Natasha Sharygina |
| 2026 | FM | Formally Explaining Neural Network Classification. | Toms Kolrik, Grigory Fedyukovich, Faezeh Labbaf, Fabrizio Leopardi, Natasha Sharygina, Michael Wand |
| 2026 | TACAS | Parallel SMT Solving via Iterative Tree Partitioning. | Toms Kolrik, Antti E. J. Hyvrinen, Seyedmasoud Asadzadeh, Natasha Sharygina |
| 2025 | CAV | Space Explanations of Neural Network Classification. | Faezeh Labbaf, Toms Kolrik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina |
| 2025 | IFM | CHC-Based Reachability Analysis via Cycle Summarization. | Konstantin Britikov, Grigory Fedyukovich, Natasha Sharygina |
| 2025 | TACAS | Unsatisfiability Proofs for Horn Solving. | Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofron, Natasha Sharygina |
| 2024 | CAV | SolTG: A CHC-Based Solidity Test Case Generator. | Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt, Natasha Sharygina |
| 2024 | FM | Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. | Konstantin Britikov, Martin Blicha, Natasha Sharygina, Grigory Fedyukovich |
| 2023 | CAV | The Golem Horn Solver. | Martin Blicha, Konstantin Britikov, Natasha Sharygina |
| 2023 | IFM | CHC Model Validation with Proof Guarantees. | Rodrigo Otoni, Martin Blicha, Patrick Eugster, Natasha Sharygina |
| 2023 | TACAS | Symbolic Model Checking for TLA+ Made Faster. | Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina |
| 2022 | CAV | SolCMC: Solidity Compiler's Model Checker. | Leonardo Alt, Martin Blicha, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2022 | FMCAD | Split Transition Power Abstraction for Unbounded Safety. | Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2022 | TACAS | Transition Power Abstractions for Deep Counterexample Detection. | Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2021 | DAC | Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. | Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2021 | FMCAD | Lookahead in Partitioning SMT. | Antti E. J. Hyvrinen, Matteo Marescotti, Natasha Sharygina |
| 2020 | FMCAD | Incremental Verification by SMT-based Summary Repair. | Sepideh Asadi, Martin Blicha, Antti E. J. Hyvrinen, Grigory Fedyukovich, Natasha Sharygina |
| 2020 | ISoLA | Accurate Smart Contract Verification Through Direct Modelling. | Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2020 | SAS | Farkas-Based Tree Interpolation. | Sepideh Asadi, Martin Blicha, Antti E. J. Hyvrinen, Grigory Fedyukovich, Natasha Sharygina |
| 2020 | VMCAI | A Cooperative Parallelization Approach for Property-Directed k-Induction. | Martin Blicha, Antti E. J. Hyvrinen, Matteo Marescotti, Natasha Sharygina |
| 2019 | MEMOCODE | Lattice-based SMT for program verification. | Karine Even-Mendoza, Antti E. J. Hyvrinen, Hana Chockler, Natasha Sharygina |
| 2019 | TACAS | Decomposing Farkas Interpolants. | Martin Blicha, Antti E. J. Hyvrinen, Jan Kofron, Natasha Sharygina |
| 2018 | ISoLA | Computing Exact Worst-Case Gas Consumption for Smart Contracts. | Matteo Marescotti, Martin Blicha, Antti E. J. Hyvrinen, Sepideh Asadi, Natasha Sharygina |
| 2018 | LPAR | Function Summarization Modulo Theories. | Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvrinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler |
| 2018 | LPAR | Lookahead-Based SMT Solving. | Antti E. J. Hyvrinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina |
| 2018 | LPAR | SMTS: Distributed, Visualized Constraint Solving. | Matteo Marescotti, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2017 | FMCAD | Duality-based interpolation for quantifier-free equalities and uninterpreted functions. | Leonardo Alt, Antti Eero Johannes Hyvrinen, Sepideh Asadi, Natasha Sharygina |
| 2017 | FMCAD | Designing parallel PDR. | Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvrinen, Natasha Sharygina |
| 2017 | SAT | Theory Refinement for Program Verification. | Antti E. J. Hyvrinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina |
| 2017 | TACAS | HiFrog: SMT-based Function Summarization for Software Verification. | Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2016 | ATVA | Clause Sharing and Partitioning for Cloud-Based SMT Solving. | Matteo Marescotti, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2016 | CAV | Property Directed Equivalence via Abstract Simulation. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2016 | FASE | PVAIR: Partial Variable Assignment InterpolatoR. | Pavel Janck, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvrinen, Jan Kofron, Natasha Sharygina |
| 2016 | SAT | OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. | Antti E. J. Hyvrinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina |
| 2015 | FASE | Symbolic Detection of Assertion Dependencies for Bounded Model Checking. | Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2015 | LPAR | Automated Discovery of Simulation Between Programs. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2015 | SAT | Search-Space Partitioning for Parallelizing SMT Solvers. | Antti E. J. Hyvrinen, Matteo Marescotti, Natasha Sharygina |
| 2014 | ATVA | Booster: An Acceleration-Based Verification Framework for Array Programs. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2014 | FMCAD | On interpolants and variable assignments. | Pavel Janck, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina |
| 2014 | ISSTA | Verification-aided regression testing. | Fabrizio Pastore, Leonardo Mariani, Antti Eero Johannes Hyvrinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, Ali Muhammad |
| 2014 | TACAS | Decision Procedures for Flat Array Properties. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2013 | ATVA | Interpolation Properties and SAT-Based Model Checking. | Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina |
| 2013 | DDECS | Interpolation-based model checking for efficient incremental analysis of software. | Grigory Fedyukovich, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2013 | LPAR | Acceleration-based safety decision procedure for programs with arrays. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2013 | LPAR | PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. | Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvrinen, Natasha Sharygina |
| 2013 | SAC | Using cross-entropy for satisfiability. | Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina |
| 2013 | TACAS | eVolCheck: Incremental Upgrade Checker for C. | Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina |
| 2012 | ATVA | FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. | Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina |
| 2012 | CADE | Reachability Modulo Theory Library. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | CAV | SAFARI: SMT-Based Abstraction for Arrays with Interpolants. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | CAV | Leveraging Interpolant Strength in Model Checking. | Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina |
| 2012 | FMCAD | Incremental upgrade checking by means of interpolation-based function summaries. | Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina |
| 2012 | LPAR | Lazy Abstraction with Interpolants for Arrays. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2011 | TACAS | Loop Summarization and Termination Analysis. | Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening |
| 2010 | CADE | Loopfrog - loop summarization for static analysis. | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | CAV | Termination Analysis with Compositional Transition Invariants. | Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2010 | ICCAD | Flexible interpolation with local proof transformations. | Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich |
| 2010 | MEMOCODE | A flexible schema for generating explanations in lazy theory propagation. | Roberto Bruttomesso, Edgar Pek, Natasha Sharygina |
| 2010 | TACAS | The OpenSMT Solver. | Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich |
| 2009 | ICCAD | A scalable decision procedure for fixed-width bit-vectors. | Roberto Bruttomesso, Natasha Sharygina |
| 2009 | SAC | The synergy of precise and fast abstractions for program verification. | Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich |
| 2008 | ATVA | Loop Summarization Using Abstract Transformers. | Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger |
| 2008 | TACAS | Scoot: A Tool for the Analysis of SystemC Models. | Nicolas Blanc, Daniel Kroening, Natasha Sharygina |
| 2007 | DATE | Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. | Daniel Kroening, Natasha Sharygina |
| 2007 | IFM | Automated Verification of Security Policies in Mobile Code. | Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi |
| 2007 | TACAS | VCEGAR: Verilog CounterExample Guided Abstraction Refinement. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2006 | FMCAD | Over-Approximating Boolean Programs with Unbounded Thread Creation. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2006 | TACAS | Approximating Predicate Images for Bit-Vector Logic. | Daniel Kroening, Natasha Sharygina |
| 2005 | CAV | The ComFoRT Reasoning Framework. | Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau |
| 2005 | CAV | Cogent: Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2005 | DAC | Word level predicate abstraction and refinement for verifying RTL verilog. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2005 | FM | Dynamic Component Substitutability Analysis. | Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha |
| 2005 | IFM | State/Event Software Verification for Branching-Time Specifications. | Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Jol Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith |
| 2005 | MEMOCODE | Formal verification of SystemC by automatic hardware/software partitioning. | Daniel Kroening, Natasha Sharygina |
| 2005 | TACAS | SATABS: SAT-Based Predicate Abstraction for ANSI-C. | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
| 2004 | IFM | State/Event-Based Software Model Checking. | Sagar Chaki, Edmund M. Clarke, Jol Ouaknine, Natasha Sharygina, Nishant Sinha |
| 2004 | ISoLA | Accurate Theorem Proving for Program Verification. | Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2004 | MEMOCODE | Automated, compositional and iterative deadlock detection. | Sagar Chaki, Edmund M. Clarke, Jol Ouaknine, Natasha Sharygina |
| 2003 | FASE | Model Checking Software via Abstraction of Loop Transitions. | Natasha Sharygina, James C. Browne |
| 2001 | FASE | A Formal Object-Oriented Analysis for Software Reliability: Design for Verification. | Natasha Sharygina, James C. Browne, Robert P. Kurshan |
| 2001 | FM | A Combined Testing and Verification Approach for Software Reliability. | Natasha Sharygina, Doron A. Peled |