Grigory Fedyukovich

Grigory Fedyukovich

Associate Professor · Department of Computer Science · Florida State University
Formal Methods Program Verification Program Synthesis Constrained Horn Clauses Model Checking Invariant Synthesis

I develop automated reasoning techniques for software and hardware correctness — spanning invariant synthesis, CHC solving, model checking, interpolation, and beyond. Previously Visiting Academic at Amazon Web Services (2021–2023), PostDoc at Princeton University (2017–2019) and University of Washington (2016–2017). PhD, University of Lugano, 2016 (advisor: Natasha Sharygina).

LOV262, 1017 Academic Way, Tallahassee FL 32304  
grigory@cs.fsu.edu  ·  Google Scholar ·  DBLP ·  CV

FSU Departmental Faculty Research Award 2024

Research & Publications

1
Formally Explaining Neural Network Classification SpEXplAIn
Kolárik, T., Fedyukovich, G., Labbaf, F., Leopardi, F., Sharygina, N., & Wand, M.
FM 2026, pp. 471–496. LNCS.
2
Space Explanations of Neural Network Classification SpEXplAIn
Labbaf, F., Kolárik, T., Blicha, M., Fedyukovich, G., Wand, M., & Sharygina, N.
CAV 2025, pp. 287–303. LNCS.
1
Exact Loop Bound Analysis ELBA
Riley, D., & Fedyukovich, G.
PLDI 2025, pp. 1814–1837. ACM.
2
Leveraging Program Structure for Test Case Generation Horntinuum
Zlatkin, I., & Fedyukovich, G.
ATVA 2024, pp. 137–157. Springer.
3
SolTG: A CHC-Based Solidity Test Case Generator SolTG
Britikov, K., Zlatkin, I., Fedyukovich, G., Alt, L., & Sharygina, N.
CAV 2024, pp. 466–479. Springer.
4
Maximal Quantified Precondition Synthesis for Linear Array Loops PreQSyn
Prabhu, S., Fedyukovich, G., & D'Souza, D.
ESOP 2024, pp. 245–274. Springer.
5
Weakest Precondition Inference for Non-Deterministic Linear Array Programs MaxPrANQ
Prabhu, S., D'Souza, D., Chakraborty, S., Venkatesh, R., & Fedyukovich, G.
TACAS 2024, Part II, pp. 175–195. Springer.
6
Lockstep Composition for Unbalanced Loops Alien
Hamza, A., & Fedyukovich, G.
TACAS 2023, pp. 270–288. Springer.
7
Maximizing Branch Coverage with Constrained Horn Clauses Horntinuum
Zlatkin, I., & Fedyukovich, G.
TACAS 2022, pp. 254–272. Springer.
8
Multi-phase invariant synthesis ImplCheck
Riley, D., & Fedyukovich, G.
ESEC/FSE 2022, pp. 607–619. ACM.
9
Specification Synthesis with Constrained Horn Clauses HornSpec
Prabhu, S., Fedyukovich, G., Madhukar, K., & D'Souza, D.
PLDI 2021, pp. 1203–1217. ACM.
10
Unbounded Procedure Summaries from Bounded Environments Clover
Pick, L., Fedyukovich, G., & Gupta, A.
VMCAI 2021, pp. 291–324. Springer.
11
Automating Modular Verification of Secure Information Flow Flower
Pick, L., Fedyukovich, G., & Gupta, A.
FMCAD 2020, pp. 158–168. TU Wien Academic Press.
12
Synthesizing Environment Invariants for Modular Hardware Verification Grain
Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., & Malik, S.
VMCAI 2020, pp. 202–225. Springer.
13
Quantified Invariants via Syntax-Guided Synthesis FreqHorn
Fedyukovich, G., Prabhu, S., Madhukar, K., & Gupta, A.
CAV 2019, pp. 259–277. Springer.
14
Accelerating Syntax-Guided Invariant Synthesis FreqHorn
Fedyukovich, G., & Bodik, R.
TACAS 2018, pp. 251–269. Springer.
15
Syntax-Guided Termination Analysis FreqTerm
Fedyukovich, G., Zhang, Y., & Gupta, A.
CAV 2018, pp. 124–143. Springer.
16
Solving Constrained Horn Clauses Using Syntax and Data FreqHorn
Fedyukovich, G., Prabhu, S., Madhukar, K., & Gupta, A.
FMCAD 2018, pp. 1–9. IEEE.
17
Sampling invariants from frequency distributions FreqHorn
Fedyukovich, G., Kaufman, S. J., & Bodik, R.
FMCAD 2017, pp. 100–107. IEEE.
1
CHC-Based Reachability Analysis via Cycle Summarization Golem
Britikov, K., Fedyukovich, G., & Sharygina, N.
iFM 2025, pp. 205–225. LNCS.
1
Reachability Analysis for Multiloop Programs Using Transition Power Abstraction Golem
Britikov, K., Blicha, M., Sharygina, N., && Fedyukovich, G.
FM 2024, pp. 558-576. LNCS.
2
Collaborative Inference of Combined Invariants RinGen
Kostyukov, Y., Mordvinov, D., & Fedyukovich, G.
LPAR 2023, pp. 288–305. EPiC Series in Computing.
3
Property Directed Inference of Relational Invariants RelSpacer
Mordvinov, D., & Fedyukovich, G.
FMCAD 2019, pp. 152–160. IEEE.
4
Transition Power Abstractions for Deep Counterexample Detection Golem
Blicha, M., Fedyukovich, G., Hyvarinen, A. E. J., & Sharygina, N.
TACAS 2022, pp. 524–542. Springer.
5
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types RInGen
Kostyukov, Y., Mordvinov, D., & Fedyukovich, G.
PLDI 2021, pp. 451–465. ACM.
6
Word Level Property Directed Reachability GSpacer
Govind V. K., Hari, Fedyukovich, G., & Gurfinkel, A.
ICCAD 2020, pp. 107:1–107:9. ACM.
7
Synchronizing Constrained Horn Clauses Rosette-Unbound
Mordvinov, D., & Fedyukovich, G.
LPAR-21 2017, pp. 338–355.
1
Syntactically Convex Model-Based Projection for Linear Real Arithmetic Golem
Becchi, A., Fedyukovich, G., Gurfinkel, A., & Nachmanson, L.
TACAS (1) 2026, pp. 45–65. LNCS.
2
Synthesis of Infinite-State Systems with Random Behavior JSyn
Katis, A., Fedyukovich, G., Chen, J., Greve, D., Rayadurgam, S., & Whalen, M. W.
ASE 2020, pp. 250–261. ACM.
3
Functional Synthesis with Examples AE-VAL
Fedyukovich, G., & Gupta, A.
CP 2019, pp. 547–564. Springer.
4
Lazy but Effective Functional Synthesis AE-VAL
Fedyukovich, G., Gurfinkel, A., & Gupta, A.
VMCAI 2019, pp. 92–113. Springer.
5
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts JSyn
Katis, A., Fedyukovich, G., Guo, H., Gacek, A., Backes, J., Gurfinkel, A., & Whalen, M. W.
TACAS 2018, pp. 176–193. Springer.
6
Gradual synthesis for static parallelization of single-pass array-processing programs GraSSP
Fedyukovich, G., Ahmad, M. B. S., & Bodik, R.
PLDI 2017, pp. 572–585. ACM.
7
Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions GraSSP
Fedyukovich, G., & Bodik, R.
SYNT@CAV 2016, pp. 55–66. EPTCS.
1
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs VeRefine
Hamza, A., Zavalia, L., Gurfinkel, A., Navas, J., & Fedyukovich, G.
OOPSLA 2025, pp. 3841–3868. ACM.
2
Exploiting Synchrony and Symmetry in Relational Verification Synonym
Pick, L., Fedyukovich, G., & Gupta, A.
CAV 2018, pp. 164–182. Springer.
3
Property Directed Equivalence via Abstract Simulation Niagara
Fedyukovich, G., Gurfinkel, A., & Sharygina, N.
CAV 2016, Part II, pp. 433–453. Springer.
4
Automated Discovery of Simulation Between Programs Niagara
Fedyukovich, G., Gurfinkel, A., & Sharygina, N.
LPAR-20 2015, pp. 606–621. Springer.
5
Verification-aided regression testing eVolCheck
Pastore, F., Mariani, L., Hyvarinen, A. E. J., Fedyukovich, G., Sharygina, N., Sehestedt, S., & Muhammad, A.
ISSTA 2014, pp. 37–48. ACM.
6
Incremental Verification of Compiler Optimizations Niagara
Fedyukovich, G., Gurfinkel, A., & Sharygina, N.
NFM 2014, pp. 300–306. Springer.
7
Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection FunFrog
Fedyukovich, G., & Sharygina, N.
SBMF 2014, pp. 96–112. Springer.
8
Symbolic Detection of Assertion Dependencies for Bounded Model Checking FunFrog
Fedyukovich, G., D'Iddio, A. C., Hyvarinen, A. E. J., & Sharygina, N.
FASE 2015, pp. 186–201. Springer.
1
Quick Theory Exploration for Algebraic Data Types via Program Transformations LemmaCalc
Ernst, G., & Fedyukovich, G.
iFM 2025, pp. 424–450. LNCS.
2
Solving Constrained Horn Clauses over Algebraic Data Types ADT-CHC
Zavalia, L., Chernigovskaia, L., & Fedyukovich, G.
VMCAI 2023, pp. 341–365. Springer.
3
Bridging Arrays and ADTs in Recursive Proofs ADT-CHC
Fedyukovich, G., & Ernst, G.
TACAS 2021, pp. 24–42. Springer.
4
Fold/Unfold Transformations for Fixpoint Logic Mu2CHC
Kobayashi, N., Fedyukovich, G., & Gupta, A.
TACAS 2020, pp. 195–214. Springer.
5
Lemma Synthesis for Automating Induction over Algebraic Data Types AdtInd
Yang, W., Fedyukovich, G., & Gupta, A.
CP 2019, pp. 600–617. Springer.
1
Farkas-Based Tree Interpolation HiFrog
Asadi, S., Blicha, M., Hyvarinen, A. E. J., Fedyukovich, G., & Sharygina, N.
SAS 2020, pp. 357–379. Springer.
2
Incremental Verification by SMT-based Summary Repair UpProver
Asadi, S., Blicha, M., Hyvarinen, A. E. J., Fedyukovich, G., & Sharygina, N.
FMCAD 2020, pp. 77–82. TU Wien Academic Press.
3
Function Summarization Modulo Theories HiFrog
Asadi, S., Blicha, M., Fedyukovich, G., Hyvarinen, A. E. J., Even-Mendoza, K., Sharygina, N., & Chockler, H.
LPAR-22 2018, pp. 56–75.
4
HiFrog: SMT-based Function Summarization for Software Verification HiFrog
Alt, L., Asadi, S., Chockler, H., Even-Mendoza, K., Fedyukovich, G., Hyvarinen, A. E. J., & Sharygina, N.
TACAS 2017, pp. 207–213. Springer.
5
Theory Refinement for Program Verification HiFrog
Hyvarinen, A. E. J., Asadi, S., Even-Mendoza, K., Fedyukovich, G., Chockler, H., & Sharygina, N.
SAT 2017, pp. 347–363. Springer.
6
PVAIR: Partial Variable Assignment InterpolatoR PVAIR
Jancik, P., Alt, L., Fedyukovich, G., Hyvarinen, A. E. J., Kofron, J., & Sharygina, N.
FASE 2016, pp. 419–434. Springer.
7
A Proof-Sensitive Approach for Small Propositional Interpolants PeRIPLO
Alt, L., Fedyukovich, G., Hyvarinen, A. E. J., & Sharygina, N.
VSTTE 2015, pp. 1–18. Springer.
8
eVolCheck: Incremental Upgrade Checker for C eVolCheck
Fedyukovich, G., Sery, O., & Sharygina, N.
TACAS 2013, pp. 292–307. Springer.
9
PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification PeRIPLO
Rollini, S. F., Alt, L., Fedyukovich, G., Hyvarinen, A. E. J., & Sharygina, N.
LPAR-19 2013, pp. 683–693. Springer.
10
FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization FunFrog
Sery, O., Fedyukovich, G., & Sharygina, N.
ATVA 2012, pp. 203–207. Springer.
11
Incremental upgrade checking by means of interpolation-based function summaries eVolCheck
Sery, O., Fedyukovich, G., & Sharygina, N.
FMCAD 2012, pp. 114–121. IEEE.
12
Interpolation-Based Function Summaries in Bounded Model Checking FunFrog
Sery, O., Fedyukovich, G., & Sharygina, N.
HVC 2011, pp. 160–175. Springer.

Graduate Students

Lucas Zavalía
PhD Student · Florida State University
expected graduation: 2027
Solving Constrained Horn Clauses over Algebraic Data Types (VMCAI'23)
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs (OOPSLA'25)
Daniel Riley
PhD Student · Florida State University
graduated at: 2026
Multi-phase invariant synthesis (ESEC/FSE'22)
Exact Loop Bound Analysis (PLDI'25)
Ameer Hamza
PhD Student · Florida State University
graduated at: 2026
Lockstep Composition for Unbalanced Loops (TACAS'23)
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs (OOPSLA'25)
Ilia Zlatkin
Master's Student · Florida State University
graduated at: 2023
Maximizing Branch Coverage with Constrained Horn Clauses (TACAS'22)
Leveraging Program Structure for Test Case Generation (ATVA'24)
Lidiia Chernigovskaia
Master's Student · Florida State University
Solving Constrained Horn Clauses over Algebraic Data Types (VMCAI'23)
Malachi McInvale
Master's Student · Florida State University
graduated at: 2025
Invariant generation using closed forms
Darin Debrestian
PhD Student · Florida State University
CHC solving for arrays
Yuki Zhang
Master's Student · Florida State University
graduated at: 2025
Data-dirven invariant generation

Grants & Funding

Cross Theory Rigorous Program Verification Using Constrained Horn Clauses
SNSF  ·  2025–2029  ·  PIs: Sharygina, Fedyukovich
$220,000 (FSU prortion)
PFI-TT: A Hybrid Scalable Data Management System Providing Deep Access to the Scientific Knowledge in Data Science
NSF  ·  2024–2026  ·  PIs: Gubanov, Pyayt, Fedyukovich
$550,000 total
Verification Mentoring Workshop 8, 9, and 10
NSF (Resource Grant)  ·  May 2024–May 2027  ·  PI: Fedyukovich
$100,000
A Test-Case Generator for Solidity
Ethereum Foundation  ·  May–Dec 2022  ·  PI: Fedyukovich
$21,000
Planning Grant: An Analysis Description Language for Collider Physics
CRC  ·  2022–2023  ·  PIs: Fedyukovich & Prosper
$25,000
Collaborative Research: SHF: Medium: Automated Word Level Synthesis for Hardware Code Generation and Verified Abstraction
NSF  ·  Jul 2021–Jul 2025  ·  Lead PI: Fedyukovich (FSU); Co-PI: Gupta (Princeton)
$914,882 total  ·  $499,882 FSU portion
Amazon Research Award: Applying FreqHorn to Verification of AWS C Common Programs
Amazon  ·  Jan–Dec 2021  ·  PI: Fedyukovich
$60,000
FYAP: Re-Modularization for Constrained Horn Clauses
FSU  ·  May–Aug 2020  ·  PI: Fedyukovich
$20,000

Teaching

COP4020
Programming Languages
COP4620
Introduction to Compiler Writing
COP5621
Compiler Construction
CEN4020
Software Engineering I
CIS5900
Computer Aided Verification

New Course Development:  CIS5900 — Computer Aided Verification (2019)

Service

Program Committee Member — OOPSLA'26
Program Committee Member — FMCAD'20, FMCAD'21, FMCAD'22, FMCAD'23, FMCAD'24, FMCAD'26
Program Committee Member — ATVA'18, ATVA'25, ATVA'26
Program Committee Member — PLDI'25
Program Committee Member — CAV'19, CAV'22, CAV'24
Sponsorship Chair & Fellowship Co-Chair — CAV'24
Workshop Chair — CAV'22 and CAV'25
Co-Chair — Verification Mentoring Workshop (at CAV'24 and CAV'25)
Program Committee Member — TACAS'23
Artifact Evaluation Co-Chair — TACAS'23
Program Committee Member — VMCAI'22, VMCAI'24
Program Committee Member — VSTTE'20, VSTTE'23
NSF Panelist — Grant Applications 2020 and 2024
Program Committee Member — ASE-Tools'21
Chair, Student Forum — FMCAD'19
Local Organization Chair & PC Member — RV'17 2017
Chair — Workshop on Verification and Synthesis for Software Evolution 2016, 2018