Formal Systems Laboratory

Home People Publications

© 2025. All rights reserved.
Built on 2025-05-07 15:23:57 -0500.

  • 2020-06-21: A General Approach to Define Binders Using Matching Logic was accepted to ICFP 2020.
  • 2019-03-28: Matching mu-Logic was accepted to LICS 2019.
  • 2018-12-17: Techniques for Evolution-Aware Runtime Verification was accepted to ICST 2019.
  • 2018-11-09: Xiaohong Chen gave a talk on the paper A Language-Independent Program Verification Framework at ISoLA 2018, Cyprus.
  • 2018-11-05: Xiaohong Chen and Grigore Rosu gave a joint talk on the paper A Language-Independent Approach to Smart Contract Verification at ISoLA 2018, Cyprus.
  • 2018-08-08: [http://mir.cs.illinois.edu/legunsen/ Evaluating Regression Test Selection Opportunities in a Very Large Open-Source Ecosystem] was accepted at ISSRE 2018.
  • 2018-07-25: IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
  • 2018-07-16: A Formal Verification Tool for Ethereum VM Bytecode was accepted at FSE 2018.
  • 2018-07-16: A Language-Independent Program Verification Framework was accepted at ISoLA 2018.
  • 2018-06-29: A Language-Independent Approach to Smart Contract Verification was accepted at ISoLA 2018.
  • 2018-06-11: [http://mir.cs.illinois.edu/legunsen/ Testing Probabilistic Programming Systems] was accepted at FSE 2018.
  • 2018-04-26: Xiaohong Chen received the 2018-2019 Yunni & Maxine Pao Memorial Fellowship.
  • 2018-03-30: KEVM: A Complete Semantics of the Ethereum Virtual Machine was accepted to CSF 2018.
  • 2017-12-21: Program Verification by Coinduction was accepted at ESOP 2018.
  • 2017-12-18: [http://mir.cs.illinois.edu/legunsen/pubs/HaririETAL18ApproximateTransformationsAsMutationOperators.pdf Approximate Transformations as Mutation Operators] was accepted at ICST 2018.
  • 2017-12-13: [http://mir.cs.illinois.edu/legunsen/pubs/BellETAL18DeFlaker.pdf DeFlaker: Automatically Detecting Flaky Tests] was accepted at ICSE 2018.
  • 2017-11-02: Everett Hildenbrandt presents the [https://github.com/kframework/evm-semantics KEVM work] at Devcon3, [https://www.youtube.com/watch?v=tIq_xECoicQ&index=11&list=PLaM7G4Llrb7xJT6JTFySxbpelkVS6GvCt video here].
  • 2017-10-12: {{zip 2017-10-12-LOPSTR.pptx PPTX}} Grigore Rosu gave an invited talk at LOPSTR’17.
  • 2017-10-03: Everett Hildenbrandt and Grigore Rosu and K in [https://cs.illinois.edu/news/cs-illinois-student-uses-tool-called-k-build-path-towards-more-secure-blockchains CLICK! article].
  • 2017-07-20: Everett Hildenbrandt won the IC3-Ethereum Cryto Bootcamp first-place for the KEVM semantics project [http://www.initc3.org/events/2017-07-13-IC3-Ethereum-Crypto-Boot-Camp-at-Cornell-University.html].
  • 2017-05-17: [https://github.com/kframework/p4-semantics P4K] was presented at [http://p4.org/p4-workshop-2017/ P4 Workshop 2017].
  • 2017-04-26: Owolabi Legunsen received the 2017 [https://cs.illinois.edu/about-us/awards/graduate-fellowships-awards/feng-chen-memorial-award Feng Chen Memorial Award in Software Engineering].
  • 2017-04-26: Daejun Park received the 2017 [https://cs.illinois.edu/about-us/awards/graduate-fellowships-awards/feng-chen-memorial-award Feng Chen Memorial Award].
  • 2017-03-16: Everett Hildenbrandt received an Honorable Mention in the 2017 [https://www.nsfgrfp.org/ NSF Graduate Research Fellowship Program (GRFP) Fellowship.].
  • 2017-03-16: Lucas Peña received the 2017 [https://www.nsfgrfp.org/ NSF Graduate Research Fellowship Program (GRFP) Fellowship.].
  • 2017-02-12: The News-Gazette [http://www.news-gazette.com/news/business/2017-02-12/wired-cosmin-radoi.html interviewed Cosmin Radoi].
  • 2016-12-01: Brandon Moore completed his Ph.D.
  • 2016-11-03: Semantics-Based Program Verifiers for All Languages won the Distinguished Paper Award at OOPSLA 2016.
  • 2016-09-02: Grigore Rosu won the [http://premii.ad-astra.ro/ Ad Astra 2016 award] for excellence in mathematics and computer science research.
  • 2016-09-01: Cosmin Radoi and Andrei Stefanescu participated in the [http://www.nsf.gov/news/special_reports/i-corps/ NSF I-Corps] program.
  • 2016-08-25: Grigore Rosu, together with his former NASA colleague Klaus Havelund, won the [http://ase-conferences.org/Mip.html ASE 2016 Most Influential Paper award] for their ASE 2001 paper Monitoring Programs using Rewriting.
  • 2016-08-16: Xiaohong Chen joined FSL.
  • 2016-07-28: How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications has received the [http://www.sigsoft.org/awards/distinguishedPaperAward.html ACM Distinguished Paper Award] at ASE 2016.
  • 2016-07-15: Cosmin Radoi will receive an [http://www.research.ibm.com/university/awards/phdfellowship.shtml IBM Ph.D. Fellowship] for the 2016-2017 academic year.
  • 2016-07-07: How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications was accepted at ASE 2016.
  • 2016-05-29: Semantics-Based Program Verifiers for All Languages was accepted at OOPSLA 2016.
  • 2016-05-13: Andrei Stefanescu passed his final defense.
  • 2016-01-15: A Language-Independent Proof System for Full Program Equivalence was accepted to be published in the Journal of Formal Aspects of Computing
  • 2015-09-12: Language Definitions as Rewrite Theories was accepted to be published in the Journal of Logical and Algebraic Methods in Programming.
  • 2015-02-16: Term-Generic Logic was accepted to be published in the Journal of Theoretical Computer Science.
  • 2015-02-08: Program Verification by Coinduction Technical report on Program Verification by Coinduction.
  • 2015-02-02: Defining the Undefinedness of C was accepted at PLDI’15.
  • 2015-02-02: KJS: A Complete Formal Semantics of JavaScript was accepted at PLDI’15.
  • 2015-01-19: Evolution-Aware Monitoring-Oriented Programming was accepted at ICSE NIER’15.
  • 2014-12-22: GPredict: Generic Predictive Concurrency Analysis was accepted at ICSE’15.
  • 2014-10-27: JavaMOP version 4.0 was released.
  • 2014-09-30: K-Java: A Complete Semantics of Java was accepted at POPL’15.
  • 2014-09-23: ROSRV: Runtime Verification for Robots was presented at RV’14 by Cansu Erdogan.