I am an Assistant Professor at Florida State University. I completed my Ph.D. at the University of Lugano under the supervision of Prof Natasha Sharygina and then a postdoc at the University of Washington with Prof Rastislav Bodik and at Princeton University with Prof Aarti Gupta.

Main directions of my research:

• Synthesis of inductive invariants for verification of program safety and termination,

• Functional (Skolem) synthesis via lazy quantifier elimination and programming by example,

• Relational verification and its applications to security analysis and automated parallelization,

• SMT-based reasoning over Algebraic Data Types: synthesis of invariants and simulation relations.

News:

• I will serve as a workshop chair and a program committee member of the 34th International Conference on Computer Aided Verification (CAV, August 7-10, 2022, Israel).




• I will serve as a program committee member of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC, 7-10 December, 2021, virtual).




• I will serve as a program committee member of the Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE, 18 - 19 Oct, 2021, virtual).




• Two papers were accepted to the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '21):

  • Specification Synthesis with Constrained Horn Clauses (distinguished)

  • Beyond the Elementary Representations of Program Invariants over Algebraic Data Types




• I will serve as a program committee member of the Tool Demonstrations track of the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE '21, November 15 - 19, 2021 Melbourne, Australia).




• I will serve as a program committee member of the 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS, 28 March 2021, virtual) and a co-organizer of the 4th CHC-COMP.




• The paper "Bridging Arrays and ADTs in Recursive Proofs" was accepted to the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21).




• The paper "Unbounded Procedure Summaries from Bounded Environments" was accepted to the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '21).




• I will serve as a program committee member of the International Workshop on Verification and Program Transformation (VPT '21, March 27 - 28, 2021, Luxembourg).




• I will serve as a program committee member of the International Conference on Formal Methods in Computer-Aided Design (FMCAD '21, October 19 - 22, 2021, Yale University, New Haven, CT).




• I will serve as a program committee member of the 27th International SPIN Symposium on Model Checking of Software (SPIN '21, July 12 - 16, 2021, Aarhus, Denmark).




• The paper "Synthesis of Infinite-State Systems with Random Behavior" was accepted to the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE '20).




• The paper "Word Level Property Directed Reachability" was accepted to the 39th International Conference On Computer Aided Design (ICCAD '20).




• The paper "Farkas-Based Tree Interpolation" was accepted to the 27th Static Analysis Symposium (SAS '20).




• Two papers were accepted to the International Conference on Formal Methods in Computer-Aided Design (FMCAD '20):

  • Automating Modular Verification of Secure Information Flow

  • Incremental Verification by SMT-based Summary Repair




• I will serve as a program committee member of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '21, 17 - 22, January, 2021, Copenhagen, Denmark).




• I will serve as a program committee member of the Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE, 19 - 20 July, 2020, Los Angeles, California, USA).




• I will serve as a reviewer of NSF proposals in 2020.




• The paper "Fold/Unfold Transformations for Fixpoint Logic" was accepted to the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20).




• I will serve as a program committee member of the 7th Workshop on Horn Clauses for Verification and Synthesis (HCVS, 26 April 2020 - Dublin, Ireland).




• I will serve as a program committee member of the International Conference on Formal Methods in Computer-Aided Design (FMCAD, September 21 - 24, 2020 - Haifa, Israel).




• The paper "Synthesizing Environment Invariants for Modular Hardware Verification" was accepted to the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '20).




• The paper "Property Directed Inference of Relational Invariants" was accepted to the International Conference on Formal Methods in Computer-Aided Design (FMCAD '19).




• Two papers were accepted to the 25th International Conference on Principles and Practice of Constraint Programming (CP '19):

  • Functional Synthesis with Examples

  • Lemma Synthesis for Automating Induction over Algebraic Data Types




• The paper "Quantified Invariants via Syntax-Guided Synthesis" was accepted to the 31st International Conference on Computer Aided Verification (CAV '19).




• The second Competition on Constrained Horn Solving is over, and its description appeared in our TACAS '19 paper on TOOLympics. Check out the results here.




• I will serve as a chair of the Student Forum of the International Conference on Formal Methods in Computer-Aided Design (FMCAD '19, San Jose, CA, USA).




• The paper "Lazy but Effective Functional Synthesis" was accepted to the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '19).




• I will serve as a program committee member of the 7th International Workshop on Verification and Program Transformation (VPT, April 2, 2019 - Genova, Italy).




• I will serve as a program co-chair of the 6th workshop on Horn Clauses for Verification and Synthesis, collocated with ETAPS (HCVS, April 6 - 11, 2019 - Prague, Czech Republic).




• The paper "Function Summarization Modulo Theories" was accepted to the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-22).




• I will serve as a program committee member of the 31st International Conference on Computer Aided Verification (CAV, July 13 - 18, 2019 - NYC, USA).




• The paper "Solving Constrained Horn Clauses Using Syntax and Data" was accepted to the International Conference on Formal Methods in Computer-Aided Design (FMCAD '18).




• Two papers were accepted to the 30th International Conference on Computer Aided Verification (CAV '18):

  • Syntax-Guided Termination Analysis

  • Exploiting Synchrony and Symmetry in Relational Verification




• I will serve as an organization committee member of the first Competition on Constrained Horn Solving, collocated with FLoC (July 6-19, 2018 - Oxford, UK).




• I will serve as a program committee member of the International Symposium on Automated Technology for Verification and Analysis (ATVA, October 7 - 10, 2018 - Los Angeles, USA).




• Two papers were accepted to the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '18):

  • Accelerating Syntax-Guided Invariant Synthesis

  • Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts




• I will serve as an artifact evaluation committee member of the 30th International Conference on Computer Aided Verification (CAV, July 14-17, 2018 - Oxford, UK).




• The paper "Sampling Invariants from Frequency Distributions" was accepted to the International Conference on Formal Methods in Computer-Aided Design (FMCAD '17), and its extended version was invited for a Special Issue on FMCAD of the Formal Methods in Systems Design (FMSD) journal.




• I will serve as a program chair of the workshop on Verification and Synthesis for Software Evolution, collocated with ETAPS (April 14-21, 2018 - Thessaloniki, Greece).




• I will attend the Dagstuhl Seminar 18151 on Program Equivalence (April 8-13, 2018 - Schloss Dagstuhl, Germany).




• The paper "Theory Refinement for Program Verification" was accepted to the International Conference on Theory and Applications of Satisfiability Testing (SAT '17).




• I will serve as a program committee member of the 4th Workshop on Horn Clauses for Verification and Synthesis (Aug 7, 2017 - Gothenburg, Sweden).




• The paper "Synchronizing Constrained Horn Clauses" was accepted to the 21st International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-21).




• The paper "Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs" was accepted to the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '17).




• The paper "HiFrog: SMT-based Function Summarization for Software Verification" was accepted to the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17).




• I will serve as a local organization chair and a program committee member of the International Conference on Runtime Verification (September 12 - 16 2017, Seattle, USA).




• ...

I (sub-)reviewed submissions at FMCAD '21, ASE-Tools '21, VSTTE '21, SYNASC '21, CAV '21, LICS '21, TACAS '21, TOPLAS '21, TSE '21, VMCAI '21, FMCAD '20, VSTTE '20, JLAMP '20, CAV '20, TACAS '20, CAV '19, NFM '19, TOSEM '19 (+1), TSE '19, SQJO '19, VPT '19, FMCAD '18, ATVA '18, SPIN '18, TOPLAS '18, TOSEM '18, CAV '18, TACAS '18, HVC '17, FMCAD '17, HCVS '17, RV '17, SAS '17, SEFM '17, CAV '17, TACAS '17, FM '16, FMCAD '16, VSTTE '16 (including selected journal submissions), CAV '16, HCVS '16, TACAS '16 (including selected journal submissions), FMCAD '15, CAV '15, FM '15, NFM '15, TACAS '15, JAR-Interpolation '14, CAV '14, PSI '14, FMCAD '14, TACAS '14, FMCAD '13, TACAS '13, VSSE '13, DATE '12, FMCAD '12, GandALF '12, CAV '12, VSTTE '12, FMCAD '11, MEMOCODE '11, and TACAS '11.

I served as the co-chair of HCVS '19, the program chair of VSSE '18 and VSSE '16, the local organization chair of RV '17, and the organization committee member of VSSE '14, CAV '13, FMCAD '10, and AVM '10.

Last update: Oct 2021