Natasha Sharygina

143 papers A* 9A 15B 32C 6Misc 2Journal 25Unranked 41

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Parallel SMT Solving via Iterative Tree Partitioning. TACAS (1) Tomás Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh, Natasha Sharygina
2025	B	`conf`	CHC-Based Reachability Analysis via Cycle Summarization. iFM Konstantin Britikov, Grigory Fedyukovich, Natasha Sharygina
2025	J	`jnl`	Golem: a flexible and efficient solver for constrained Horn clauses. Formal Methods Syst. Des. Martin Blicha, Konstantin Britikov, Natasha Sharygina
2025	—	`conf`	Space Explanations of Neural Network Classification. CAV (3) Faezeh Labbaf, Tomás Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
2025	J	`jnl`	Space Explanations of Neural Network Classification. CoRR Faezeh Labbaf, Tomás Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
2025	—	`conf`	Unsatisfiability Proofs for Horn Solving. TACAS (2) Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofron, Natasha Sharygina
2025	J	`jnl`	Validation of CHC Satisfiability with ATHENA. Formal Aspects Comput. Rodrigo Otoni, Martin Blicha, Patrick Eugster, Natasha Sharygina
2024	—	`conf`	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. FM (1) Konstantin Britikov, Martin Blicha, Natasha Sharygina, Grigory Fedyukovich
2024	—	`conf`	SolTG: A CHC-Based Solidity Test Case Generator. CAV (1) Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt, Natasha Sharygina
2023	J	`jnl`	A Solicitous Approach to Smart Contract Verification. ACM Trans. Priv. Secur. Rodrigo Otoni, Matteo Marescotti, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
2023	B	`conf`	CHC Model Validation with Proof Guarantees. iFM Rodrigo Otoni, Martin Blicha, Patrick Eugster, Natasha Sharygina
2023	—	`conf`	Picky CDCL: SMT-Solving with Flexible Literal Selection. VSTTE Konstantin Britikov, Antti E. J. Hyvärinen, Natasha Sharygina
2023	—	`conf`	Symbolic Model Checking for TLA+ Made Faster. TACAS (1) Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina
2023	—	`conf`	The Golem Horn Solver. CAV (2) Martin Blicha, Konstantin Britikov, Natasha Sharygina
2023	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I TACAS (1) Sriram Sankaranarayanan, Natasha Sharygina
2023	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II TACAS (2) Sriram Sankaranarayanan, Natasha Sharygina
2022	J	`jnl`	SMT-based verification of program changes through summary repair. Formal Methods Syst. Des. Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
2022	—	`ed.`	Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers VSTTE Roderick Bloem, Rayna Dimitrova, Chuchu Fan, Natasha Sharygina
2022	—	`conf`	SolCMC: Solidity Compiler's Model Checker. CAV (1) Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, Natasha Sharygina
2022	B	`conf`	Split Transition Power Abstraction for Unbounded Safety. FMCAD Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2022	—	`conf`	Transition Power Abstractions for Deep Counterexample Detection. TACAS (1) Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2022	J	`jnl`	Using linear algebra in decomposition of Farkas interpolants. Int. J. Softw. Tools Technol. Transf. Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
2021	B	`conf`	Lookahead in Partitioning SMT. FMCAD Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
2021	A*	`conf`	Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. DAC Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
2020	B	`conf`	A Cooperative Parallelization Approach for Property-Directed k-Induction. VMCAI Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
2020	—	`conf`	Accurate Smart Contract Verification Through Direct Modelling. ISoLA (3) Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina
2020	B	`conf`	Farkas-Based Tree Interpolation. SAS Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
2020	B	`conf`	Incremental Verification by SMT-based Summary Repair. FMCAD Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
2019	—	`conf`	Decomposing Farkas Interpolants. TACAS (1) Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
2019	J	`jnl`	Exploiting partial variable assignment in interpolation-based model checking. Formal Methods Syst. Des. Pavel Jancík, Jan Kofron, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2019	C	`conf`	Lattice-based SMT for program verification. MEMOCODE Karine Even-Mendoza, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina
2018	—	`conf`	Computing Exact Worst-Case Gas Consumption for Smart Contracts. ISoLA (4) Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi, Natasha Sharygina
2018	B	`conf`	Function Summarization Modulo Theories. LPAR Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler
2018	—	`conf`	Lattice-Based Refinement in Bounded Model Checking. VSTTE Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina
2018	B	`conf`	Lookahead-Based SMT Solving. LPAR Antti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina
2018	—	`ch.`	Modeling for Verification. Handbook of Model Checking Sanjit A. Seshia, Natasha Sharygina, Stavros Tripakis
2018	B	`conf`	SMTS: Distributed, Visualized Constraint Solving. LPAR Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
2017	J	`jnl`	A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Informaticae Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2017	B	`conf`	Designing parallel PDR. FMCAD Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina
2017	B	`conf`	Duality-based interpolation for quantifier-free equalities and uninterpreted functions. FMCAD Leonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina
2017	J	`jnl`	Flexible SAT-based framework for incremental bounded upgrade checking. Int. J. Softw. Tools Technol. Transf. Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
2017	—	`conf`	HiFrog: SMT-based Function Summarization for Software Verification. TACAS (2) Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2017	—	`conf`	LRA Interpolants from No Man's Land. Haifa Verification Conference Leonardo Alt, Antti E. J. Hyvärinen, Natasha Sharygina
2017	A	`conf`	Theory Refinement for Program Verification. SAT Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina
2017	—	`conf`	Visualising SMT-Based Parallel Constraint Solving. SMT Jelena Budakovic, Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
2016	B	`conf`	Clause Sharing and Partitioning for Cloud-Based SMT Solving. ATVA Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
2016	A	`conf`	OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. SAT Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina
2016	B	`conf`	PVAIR: Partial Variable Assignment InterpolatoR. FASE Pavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
2016	—	`conf`	Property Directed Equivalence via Abstract Simulation. CAV (2) Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2015	—	`conf`	A New Acceleration-Based Combination Framework for Array Properties. FroCos Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2015	—	`conf`	A Proof-Sensitive Approach for Small Propositional Interpolants. VSTTE Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2015	B	`conf`	Automated Discovery of Simulation Between Programs. LPAR Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2015	—	`ch.`	Challenges of Existing Technology. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	—	`ch.`	Complementarities Among the Technologies Presented in the Book. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	J	`jnl`	Decision Procedures for Flat Array Properties. J. Autom. Reason. Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2015	—	`conf`	Flexible Interpolation for Efficient Model Checking. MEMICS Antti E. J. Hyvärinen, Leonardo Alt, Natasha Sharygina
2015	—	`ch.`	Function Summarization-Based Bounded Model Checking. Validation of Evolving Software Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
2015	—	`ch.`	Incremental Upgrade Checking. Validation of Evolving Software Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
2015	—	`ch.`	Introduction. Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2015	—	`ch.`	Optimizing Function Summaries Through Interpolation. Validation of Evolving Software Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina
2015	—	`ch.`	Regression Checking of Changes in C Software. Validation of Evolving Software Fabrizio Pastore, Leonardo Mariani, Antti Eero Johannes Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, Ali Muhammad
2015	A	`conf`	Search-Space Partitioning for Parallelizing SMT Solvers. SAT Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
2015	B	`conf`	Symbolic Detection of Assertion Dependencies for Bounded Model Checking. FASE Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, Natasha Sharygina
2015	—	`book`	Validation of Evolving Software Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
2014	—	`conf`	A Framework for the Verification of Parameterized Infinite-State Systems. CILC Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	J	`jnl`	An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2014	B	`conf`	Booster: An Acceleration-Based Verification Framework for Array Programs. ATVA Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	—	`conf`	Decision Procedures for Flat Array Properties. SMT Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	A	`conf`	Decision Procedures for Flat Array Properties. TACAS Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	—	`conf`	Incremental Verification of Compiler Optimizations. NASA Formal Methods Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2014	—	`conf`	Monotonic Abstraction Techniques: from Parametric to Software Model Checking. MOD* Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2014	B	`conf`	On interpolants and variable assignments. FMCAD Pavel Jancík, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina
2014	J	`jnl`	Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
2014	—	`conf`	Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection. SBMF Grigory Fedyukovich, Natasha Sharygina
2014	A	`conf`	Verification-aided regression testing. ISSTA Fabrizio Pastore, Leonardo Mariani, Antti Eero Johannes Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, Ali Muhammad
2014	—	`conf`	Verige: verification with invariant generation engine. SPIN Nicolas Latorre, Francesco Alberti, Natasha Sharygina
2013	—	`conf`	A Parametric Interpolation Framework for First-Order Theories. MICAI (1) Laura Kovács, Simone Fulvio Rollini, Natasha Sharygina
2013	J	`jnl`	Abstraction and Acceleration in SMT-based Model-Checking for Array Programs CoRR Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	—	`conf`	Acceleration-based safety decision procedure for programs with arrays. LPAR (short papers) Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	A*	`ed.`	Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings CAV Natasha Sharygina, Helmut Veith
2013	—	`conf`	Definability of Accelerated Relations in a Theory of Arrays and Its Applications. FroCos Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
2013	B	`conf`	Interpolation Properties and SAT-Based Model Checking. ATVA Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
2013	C	`conf`	Interpolation-based model checking for efficient incremental analysis of software. DDECS Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
2013	J	`jnl`	Loop summarization using state and transition invariants. Formal Methods Syst. Des. Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2013	—	`conf`	PINCETTE - Validating Changes and Upgrades in Networked Software. CSMR 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
2013	B	`conf`	PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. LPAR Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina
2013	J	`jnl`	Resolution Proof Transformation for Compression and Interpolation. CoRR Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
2013	Misc	`conf`	Using cross-entropy for satisfiability. SAC Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina
2013	A	`conf`	eVolCheck: Incremental Upgrade Checker for C. TACAS Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
2012	J	`jnl`	An abstraction refinement approach combining precise and approximated techniques. Int. J. Softw. Tools Technol. Transf. Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
2012	B	`conf`	FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. ATVA Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
2012	B	`conf`	Incremental upgrade checking by means of interpolation-based function summaries. FMCAD Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
2012	B	`conf`	Lazy Abstraction with Interpolants for Arrays. LPAR Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012	A*	`conf`	Leveraging Interpolant Strength in Model Checking. CAV Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina
2012	J	`jnl`	Propositional Interpolation Systems for Model Checking CoRR Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
2012	—	`conf`	Reachability Modulo Theory Library. SMT@IJCAR Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012	A*	`conf`	SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2011	J	`jnl`	A model checking-based approach for security policy verification of mobile systems. Formal Aspects Comput. Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi
2011	—	`conf`	Function Summaries in Software Upgrade Checking. Haifa Verification Conference Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
2011	—	`conf`	Interpolation-Based Function Summaries in Bounded Model Checking. Haifa Verification Conference Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
2011	A	`conf`	Loop Summarization and Termination Analysis. TACAS Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening
2010	C	`conf`	A flexible schema for generating explanations in lazy theory propagation. MEMOCODE Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
2010	—	`conf`	An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference Simone Rollini, Roberto Bruttomesso, Natasha Sharygina
2010	A	`conf`	Flexible interpolation with local proof transformations. ICCAD Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich
2010	—	`conf`	Loopfrog - loop summarization for static analysis. WING@ETAPS/IJCAR Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2010	B	`ed.`	Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23 FMCAD Roderick Bloem, Natasha Sharygina
2010	A*	`conf`	Termination Analysis with Compositional Transition Invariants. CAV Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
2010	A	`conf`	The OpenSMT Solver. TACAS Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich
2009	A	`conf`	A scalable decision procedure for fixed-width bit-vectors. ICCAD Roberto Bruttomesso, Natasha Sharygina
2009	—	`conf`	An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk. SAVCBS Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
2009	A*	`conf`	Loopfrog: A Static Analyzer for ANSI-C Programs. ASE Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2009	Misc	`conf`	The synergy of precise and fast abstractions for program verification. SAC Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich
2008	B	`conf`	Loop Summarization Using Abstract Transformers. ATVA Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
2008	A	`conf`	Scoot: A Tool for the Analysis of SystemC Models. TACAS Nicolas Blanc, Daniel Kroening, Natasha Sharygina
2008	J	`jnl`	Verification of evolving software via component substitutability analysis. Formal Methods Syst. Des. Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
2008	J	`jnl`	Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	B	`conf`	Automated Verification of Security Policies in Mobile Code. IFM Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi
2007	A	`conf`	Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs. DATE Daniel Kroening, Natasha Sharygina
2007	—	`ch.`	Model Checking with Abstraction for Web Services. Test and Analysis of Web Services Natasha Sharygina, Daniel Kröning
2007	—	`conf`	Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE Jonathan Aldrich, Michael Barnett, Dimitra Giannakopoulou, Gary T. Leavens, Natasha Sharygina
2007	A	`conf`	VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	J	`jnl`	Verification of Boolean programs with unbounded thread creation. Theor. Comput. Sci. Byron Cook, Daniel Kroening, Natasha Sharygina
2006	A	`conf`	Approximating Predicate Images for Bit-Vector Logic. TACAS Daniel Kroening, Natasha Sharygina
2006	B	`conf`	Over-Approximating Boolean Programs with Unbounded Thread Creation. FMCAD Byron Cook, Daniel Kroening, Natasha Sharygina
2005	A*	`conf`	Cogent: Accurate Theorem Proving for Program Verification. CAV Byron Cook, Daniel Kroening, Natasha Sharygina
2005	J	`jnl`	Concurrent software verification with states, events, and deadlocks. Formal Aspects Comput. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha
2005	B	`conf`	Dynamic Component Substitutability Analysis. FM Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha
2005	C	`conf`	Formal verification of SystemC by automatic hardware/software partitioning. MEMOCODE Daniel Kroening, Natasha Sharygina
2005	—	`conf`	Program Compatibility Approaches. FMCO Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
2005	A	`conf`	SATABS: SAT-Based Predicate Abstraction for ANSI-C. TACAS Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2005	B	`conf`	State/Event Software Verification for Branching-Time Specifications. IFM Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith
2005	—	`conf`	Symbolic Model Checking for Asynchronous Boolean Programs. SPIN Byron Cook, Daniel Kroening, Natasha Sharygina
2005	A*	`conf`	The ComFoRT Reasoning Framework. CAV Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau
2005	A*	`conf`	Word level predicate abstraction and refinement for verifying RTL verilog. DAC Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2004	C	`conf`	Accurate Theorem Proving for Program Verification. ISoLA Byron Cook, Daniel Kroening, Natasha Sharygina
2004	C	`conf`	Automated, compositional and iterative deadlock detection. MEMOCODE Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina
2004	J	`jnl`	Guest Editorial. Formal Methods Syst. Des. Natasha Sharygina
2004	J	`jnl`	Lessons Learned from Model Checking a NASA Robot Controller. Formal Methods Syst. Des. Natasha Sharygina, James C. Browne, Fei Xie, Robert P. Kurshan, Vladimir Levin
2004	J	`jnl`	Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods Syst. Des. Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2004	B	`conf`	State/Event-Based Software Model Checking. IFM Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha
2003	B	`conf`	Model Checking Software via Abstraction of Loop Transitions. FASE Natasha Sharygina, James C. Browne
2001	—	`conf`	A Combined Testing and Verification Approach for Software Reliability. FME Natasha Sharygina, Doron A. Peled
2001	B	`conf`	A Formal Object-Oriented Analysis for Software Reliability: Design for Verification. FASE Natasha Sharygina, James C. Browne, Robert P. Kurshan