Grigory Fedyukovich

82 papers A* 5A 6B 23C 1Misc 1Journal 12Unranked 29

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Syntactically Convex Model-Based Projection for Linear Real Arithmetic. TACAS (1) Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson
2025	J	`jnl`	A Flow-Sensitive Refinement Type System for Verifying eBPF Programs. Proc. ACM Program. Lang. Ameer Hamza, Lucas Zavalía, Arie Gurfinkel, Jorge A. Navas, Grigory Fedyukovich
2025	B	`conf`	CHC-Based Reachability Analysis via Cycle Summarization. iFM Konstantin Britikov, Grigory Fedyukovich, Natasha Sharygina
2025	J	`jnl`	Exact Loop Bound Analysis. Proc. ACM Program. Lang. Daniel Riley, Grigory Fedyukovich
2025	B	`conf`	Quick Theory Exploration for Algebraic Data Types via Program Transformations. iFM Gidon Ernst, Grigory Fedyukovich
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
2024	—	`conf`	Leveraging Program Structure for Test Case Generation. ATVA (2) Ilia Zlatkin, Grigory Fedyukovich
2024	—	`conf`	Maximal Quantified Precondition Synthesis for Linear Array Loops. ESOP (2) Sumanth Prabhu, Grigory Fedyukovich, Deepak D'Souza
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
2024	—	`conf`	Weakest Precondition Inference for Non-Deterministic Linear Array Programs. TACAS (2) Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, R. Venkatesh, Grigory Fedyukovich
2023	B	`conf`	Collaborative Inference of Combined Invariants. LPAR Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
2023	—	`conf`	Lockstep Composition for Unbalanced Loops. TACAS (2) Ameer Hamza, Grigory Fedyukovich
2023	B	`conf`	Solving Constrained Horn Clauses over Algebraic Data Types. VMCAI Lucas Zavalía, Lidiia Chernigovskaia, Grigory Fedyukovich
2022	A*	`conf`	Horntinuum: Autonomous Testing using Constrained Horn Clauses. ASE Ilia Zlatkin, Grigory Fedyukovich
2022	—	`conf`	Maximizing Branch Coverage with Constrained Horn Clauses. TACAS (2) Ilia Zlatkin, Grigory Fedyukovich
2022	—	`conf`	Multi-phase invariant synthesis. ESEC/SIGSOFT FSE Daniel Riley, Grigory Fedyukovich
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	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
2021	J	`jnl`	Beyond the Elementary Representations of Program Invariants over Algebraic Data Types. CoRR Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
2021	A*	`conf`	Beyond the elementary representations of program invariants over algebraic data types. PLDI Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
2021	—	`conf`	Bridging Arrays and ADTs in Recursive Proofs. TACAS (2) Grigory Fedyukovich, Gidon Ernst
2021	—	`conf`	Competition Report: CHC-COMP-21. HCVS@ETAPS Grigory Fedyukovich, Philipp Rümmer
2021	A*	`conf`	Specification synthesis with constrained Horn clauses. PLDI Sumanth Prabhu S, Grigory Fedyukovich, Kumar Madhukar, Deepak D'Souza
2021	B	`conf`	Unbounded Procedure Summaries from Bounded Environments. VMCAI Lauren Pick, Grigory Fedyukovich, Aarti Gupta
2020	B	`conf`	Automating Modular Verification of Secure Information Flow. FMCAD Lauren Pick, Grigory Fedyukovich, Aarti Gupta
2020	B	`conf`	Farkas-Based Tree Interpolation. SAS Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
2020	—	`conf`	Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
2020	B	`conf`	Incremental Verification by SMT-based Summary Repair. FMCAD Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
2020	J	`jnl`	Learning inductive invariants by sampling from frequency distributions. Formal Methods Syst. Des. Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík
2020	A*	`conf`	Synthesis of Infinite-State Systems with Random Behavior. ASE Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
2020	J	`jnl`	Synthesis of Infinite-State Systems with Random Behavior. CoRR Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
2020	B	`conf`	Synthesizing Environment Invariants for Modular Hardware Verification. VMCAI Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik
2020	A	`conf`	Word Level Property Directed Reachability. ICCAD Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel
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	A	`conf`	Functional Synthesis with Examples. CP Grigory Fedyukovich, Aarti Gupta
2019	B	`conf`	Lazy but Effective Functional Synthesis. VMCAI Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
2019	A	`conf`	Lemma Synthesis for Automating Induction over Algebraic Data Types. CP Weikun Yang, Grigory Fedyukovich, Aarti Gupta
2019	—	`ed.`	Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, HCVS/PERR@ETAPS 2019, Prague, Czech Republic, 6-7th April 2019. HCVS/PERR@ETAPS Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos, Mattias Ulbrich
2019	B	`conf`	Property Directed Inference of Relational Invariants. FMCAD Dmitry Mordvinov, Grigory Fedyukovich
2019	—	`conf`	Quantified Invariants via Syntax-Guided Synthesis. CAV (1) Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
2019	—	`conf`	TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) 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
2019	B	`conf`	The FMCAD 2019 Student Forum. FMCAD Grigory Fedyukovich
2018	—	`conf`	Accelerating Syntax-Guided Invariant Synthesis. TACAS (1) Grigory Fedyukovich, Rastislav Bodík
2018	—	`conf`	Exploiting Synchrony and Symmetry in Relational Verification. CAV (1) Lauren Pick, Grigory Fedyukovich, Aarti Gupta
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	B	`conf`	Solving Constrained Horn Clauses Using Syntax and Data. FMCAD Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
2018	—	`conf`	Syntax-Guided Termination Analysis. CAV (1) Grigory Fedyukovich, Yueling Zhang, Aarti Gupta
2018	—	`conf`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
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	A*	`conf`	Gradual synthesis for static parallelization of single-pass array-processing programs. PLDI Grigory Fedyukovich, Maaz Bin Safeer Ahmad, Rastislav Bodík
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	B	`conf`	Sampling invariants from frequency distributions. FMCAD Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík
2017	B	`conf`	Synchronizing Constrained Horn Clauses. LPAR Dmitry Mordvinov, Grigory Fedyukovich
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	J	`jnl`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
2017	J	`jnl`	Verifying Safety of Functional Programs with Rosette/Unbound. CoRR Dmitry Mordvinov, Grigory Fedyukovich
2016	—	`conf`	Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions. SYNT@CAV Grigory Fedyukovich, Rastislav Bodík
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
2016	J	`jnl`	Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
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.`	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.`	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	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
2014	—	`conf`	Incremental Verification of Compiler Optimizations. NASA Formal Methods Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
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
2013	C	`conf`	Interpolation-based model checking for efficient incremental analysis of software. DDECS Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina
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	A	`conf`	eVolCheck: Incremental Upgrade Checker for C. TACAS Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina
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
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
2010	Misc	`conf`	Implementing Parallel Algorithms of MapReduce. PDPTA Grigory Fedyukovich, Vladimir Safonov