Grigory Fedyukovich

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 57

Top Topics

Top Venues

Publications

Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, R. Venkatesh, Grigory Fedyukovich
Weakest Precondition Inference for Non-Deterministic Linear Array Programs. TACAS (2) (2024)
Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt, Natasha Sharygina
SolTG: A CHC-Based Solidity Test Case Generator. CAV (1) (2024)
Sumanth Prabhu, Grigory Fedyukovich, Deepak D'Souza
Maximal Quantified Precondition Synthesis for Linear Array Loops. ESOP (2) (2024)
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
Collaborative Inference of Combined Invariants. LPAR (2023)
Ameer Hamza, Grigory Fedyukovich
Lockstep Composition for Unbalanced Loops. TACAS (2) (2023)
Lucas Zavalía, Lidiia Chernigovskaia, Grigory Fedyukovich
Solving Constrained Horn Clauses over Algebraic Data Types. VMCAI (2023)
Ilia Zlatkin, Grigory Fedyukovich
Maximizing Branch Coverage with Constrained Horn Clauses. TACAS (2) (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)
Ilia Zlatkin, Grigory Fedyukovich
Horntinuum: Autonomous Testing using Constrained Horn Clauses. ASE (2022)
Daniel Riley, Grigory Fedyukovich
Multi-phase invariant synthesis. ESEC/SIGSOFT FSE (2022)
Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Transition Power Abstractions for Deep Counterexample Detection. TACAS (1) (2022)
Lauren Pick, Grigory Fedyukovich, Aarti Gupta
Unbounded Procedure Summaries from Bounded Environments. VMCAI (2021)
Sumanth Prabhu S, Grigory Fedyukovich, Kumar Madhukar, Deepak D'Souza
Specification synthesis with constrained Horn clauses. PLDI (2021)
Grigory Fedyukovich, Philipp Rümmer
Competition Report: CHC-COMP-21. HCVS@ETAPS (2021)
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
Beyond the elementary representations of program invariants over algebraic data types. PLDI (2021)
Grigory Fedyukovich, Gidon Ernst
Bridging Arrays and ADTs in Recursive Proofs. TACAS (2) (2021)
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types. CoRR (2021)
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
Solving Constrained Horn Clauses over ADTs by Finite Model Finding. CoRR (2021)
Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík
Learning inductive invariants by sampling from frequency distributions. Formal Methods Syst. Des. 56 (1) (2020)
Lauren Pick, Grigory Fedyukovich, Aarti Gupta
Automating Modular Verification of Secure Information Flow. FMCAD (2020)
Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel
Word Level Property Directed Reachability. ICCAD (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)
Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) (2020)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. ASE (2020)
Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik
Synthesizing Environment Invariants for Modular Hardware Verification. VMCAI (2020)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. CoRR (2020)
Weikun Yang, Grigory Fedyukovich, Aarti Gupta
Lemma Synthesis for Automating Induction over Algebraic Data Types. CP (2019)
Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
Lazy but Effective Functional Synthesis. VMCAI (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)
Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
Quantified Invariants via Syntax-Guided Synthesis. CAV (1) (2019)
Dmitry Mordvinov, Grigory Fedyukovich
Property Directed Inference of Relational Invariants. FMCAD (2019)
Grigory Fedyukovich
The FMCAD 2019 Student Forum. FMCAD (2019)
Grigory Fedyukovich, Aarti Gupta
Functional Synthesis with Examples. CP (2019)
Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) (2019)
Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler
Function Summarization Modulo Theories. LPAR (2018)
Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
Solving Constrained Horn Clauses Using Syntax and Data. FMCAD (2018)
Grigory Fedyukovich, Yueling Zhang, Aarti Gupta
Syntax-Guided Termination Analysis. CAV (1) (2018)
Lauren Pick, Grigory Fedyukovich, Aarti Gupta
Exploiting Synchrony and Symmetry in Relational Verification. CAV (1) (2018)
Grigory Fedyukovich, Rastislav Bodík
Accelerating Syntax-Guided Invariant Synthesis. TACAS (1) (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) (2018)
Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík
Sampling invariants from frequency distributions. FMCAD (2017)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR (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)
Grigory Fedyukovich, Maaz Bin Safeer Ahmad, Rastislav Bodík
Gradual synthesis for static parallelization of single-pass array-processing programs. PLDI (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)
Dmitry Mordvinov, Grigory Fedyukovich
Synchronizing Constrained Horn Clauses. LPAR (2017)
Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina
Theory Refinement for Program Verification. SAT (2017)
Dmitry Mordvinov, Grigory Fedyukovich
Verifying Safety of Functional Programs with Rosette/Unbound. CoRR (2017)
Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR (2016)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Property Directed Equivalence via Abstract Simulation. CAV (2) (2016)
Grigory Fedyukovich, Rastislav Bodík
Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions. SYNT@CAV (2016)
Pavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
PVAIR: Partial Variable Assignment InterpolatoR. FASE (2016)
Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, Natasha Sharygina
Symbolic Detection of Assertion Dependencies for Bounded Model Checking. FASE (2015)
Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
A Proof-Sensitive Approach for Small Propositional Interpolants. VSTTE (2015)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Automated Discovery of Simulation Between Programs. LPAR (2015)
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)
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)
Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
Interpolation-based model checking for efficient incremental analysis of software. DDECS (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)
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. ATVA (2012)
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
Incremental upgrade checking by means of interpolation-based function summaries. FMCAD (2012)
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)
Grigory Fedyukovich, Vladimir Safonov
Implementing Parallel Algorithms of MapReduce. PDPTA (2010)