Implementing Parallel Algorithms of MapReduce. - Grigory Fedyukovich; Vladimir Safonov (PDPTA, 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)

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

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

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)

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)

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

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)

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)

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

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

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)

Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions. - Grigory Fedyukovich; Rastislav Bodík (SYNT@CAV, 2016)

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. - Andreas Katis; Grigory Fedyukovich; Andrew Gacek; John D. Backes; Arie Gurfinkel; Michael W. Whalen (CoRR, 2016)

Sampling invariants from frequency distributions. - Grigory Fedyukovich; Samuel J. Kaufman; Rastislav Bodík (FMCAD, 2017)

Synchronizing Constrained Horn Clauses. - Dmitry Mordvinov; Grigory Fedyukovich (LPAR, 2017)

Gradual synthesis for static parallelization of single-pass array-processing programs. - Grigory Fedyukovich; Maaz Bin Safeer Ahmad; Rastislav Bodík (PLDI, 2017)

Theory Refinement for Program Verification. - Antti E. J. Hyvärinen; Sepideh Asadi; Karine Even-Mendoza; Grigory Fedyukovich; Hana Chockler; Natasha Sharygina (SAT, 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)

Verifying Safety of Functional Programs with Rosette/Unbound. - Dmitry Mordvinov; Grigory Fedyukovich (CoRR, 2017)

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

Syntax-Guided Termination Analysis. - Grigory Fedyukovich; Yueling Zhang; Aarti Gupta (CAV (1), 2018)

Exploiting Synchrony and Symmetry in Relational Verification. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (CAV (1), 2018)

Solving Constrained Horn Clauses Using Syntax and Data. - Grigory Fedyukovich; Sumanth Prabhu 001; Kumar Madhukar; Aarti Gupta (FMCAD, 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)

Accelerating Syntax-Guided Invariant Synthesis. - Grigory Fedyukovich; Rastislav Bodík (TACAS (1), 2018)

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. - Andreas Katis; Grigory Fedyukovich; Huajun Guo; Andrew Gacek; John Backes; Arie Gurfinkel; Michael W. Whalen (TACAS (2), 2018)

Quantified Invariants via Syntax-Guided Synthesis. - Grigory Fedyukovich; Sumanth Prabhu 001; Kumar Madhukar; Aarti Gupta (CAV (1), 2019)

Functional Synthesis with Examples. - Grigory Fedyukovich; Aarti Gupta (CP, 2019)

Lemma Synthesis for Automating Induction over Algebraic Data Types. - Weikun Yang; Grigory Fedyukovich; Aarti Gupta (CP, 2019)

The FMCAD 2019 Student Forum. - Grigory Fedyukovich (FMCAD, 2019)

Property Directed Inference of Relational Invariants. - Dmitry Mordvinov; Grigory Fedyukovich (FMCAD, 2019)

TOOLympics 2019: An Overview of Competitions in Formal Methods. - Ezio Bartocci; Dirk Beyer 001; Paul E. Black; Grigory Fedyukovich; Hubert Garavel; Arnd Hartmanns; Marieke Huisman; Fabrice Kordon; Julian Nagele; Mihaela Sighireanu; Bernhard Steffen; Martin Suda 001; et al. (TACAS (3), 2019)

Lazy but Effective Functional Synthesis. - Grigory Fedyukovich; Arie Gurfinkel; Aarti Gupta (VMCAI, 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)

Automating Modular Verification of Secure Information Flow. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (FMCAD, 2020)

Word Level Property Directed Reachability. - Hari Govind V. K.; Grigory Fedyukovich; Arie Gurfinkel (ICCAD, 2020)

Synthesis of Infinite-State Systems with Random Behavior. - Andreas Katis; Grigory Fedyukovich; Jeffrey Chen; David A. Greve; Sanjai Rayadurgam; Michael W. Whalen (ASE, 2020)

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

Fold/Unfold Transformations for Fixpoint Logic. - Naoki Kobayashi 001; Grigory Fedyukovich; Aarti Gupta (TACAS (2), 2020)

Synthesizing Environment Invariants for Modular Hardware Verification. - Hongce Zhang; Weikun Yang; Grigory Fedyukovich; Aarti Gupta; Sharad Malik (VMCAI, 2020)

Learning inductive invariants by sampling from frequency distributions. - Grigory Fedyukovich; Samuel J. Kaufman; Rastislav Bodík (Formal Methods Syst. Des., 2020)

Beyond the elementary representations of program invariants over algebraic data types. - Yurii Kostyukov; Dmitry Mordvinov; Grigory Fedyukovich (PLDI, 2021)

Specification synthesis with constrained Horn clauses. - Sumanth Prabhu S; Grigory Fedyukovich; Kumar Madhukar; Deepak D'Souza (PLDI, 2021)

Bridging Arrays and ADTs in Recursive Proofs. - Grigory Fedyukovich; Gidon Ernst (TACAS (2), 2021)

Unbounded Procedure Summaries from Bounded Environments. - Lauren Pick; Grigory Fedyukovich; Aarti Gupta (VMCAI, 2021)

Competition Report: CHC-COMP-21. - Grigory Fedyukovich; Philipp Rümmer (HCVS@ETAPS, 2021)

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

Horntinuum: Autonomous Testing using Constrained Horn Clauses. - Ilia Zlatkin; Grigory Fedyukovich (ASE, 2022)

Multi-phase invariant synthesis. - Daniel Riley; Grigory Fedyukovich (ESEC/SIGSOFT FSE, 2022)

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

Maximizing Branch Coverage with Constrained Horn Clauses. - Ilia Zlatkin; Grigory Fedyukovich (TACAS (2), 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)

Collaborative Inference of Combined Invariants. - Yurii Kostyukov; Dmitry Mordvinov; Grigory Fedyukovich (LPAR, 2023)

Lockstep Composition for Unbalanced Loops. - Ameer Hamza; Grigory Fedyukovich (TACAS (2), 2023)

Solving Constrained Horn Clauses over Algebraic Data Types. - Lucas Zavalía; Lidiia Chernigovskaia; Grigory Fedyukovich (VMCAI, 2023)

Leveraging Program Structure for Test Case Generation. - Ilia Zlatkin; Grigory Fedyukovich (ATVA (2), 2024)

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

Maximal Quantified Precondition Synthesis for Linear Array Loops. - Sumanth Prabhu 001; Grigory Fedyukovich; Deepak D'Souza (ESOP (2), 2024)

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

Weakest Precondition Inference for Non-Deterministic Linear Array Programs. - Sumanth Prabhu 001; Deepak D'Souza; Supratik Chakraborty; R. Venkatesh 001; Grigory Fedyukovich (TACAS (2), 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)

Exact Loop Bound Analysis. - Daniel Riley; Grigory Fedyukovich (Proc. ACM Program. Lang., 2025)