Programming Language Design and Semantics

2023

• Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

  Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and Grigore Rosu
  OOPSLA'23 ACM, July 2023
  PDF BIB OOPSLA'23 Matching Logic Proof Checker

2021

• Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

  Xiaohong Chen and Zhengyao Lin and Minh-Thai Trinh and Grigore Rosu
  CAV'21 ACM, July 2021
  PDF BIB CAV'21 Matching Logic Proof Checker

2019

• A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

  Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu
  PLDI'19 ACM, pp 1133-1148, June 2019
  PDF BIB PLDI'19 Semantics

• SETSS'19 Lecture Notes on K

  Xiaohong Chen and Grigore Rosu
  SETSS'19 Springer, 2019
  PDF BIB K

2018

• A Language-Independent Program Verification Framework

  Xiaohong Chen and Grigore Rosu
  ISoLA'18 Springer, pp 92-102, November 2018
  PDF BIB ISoLA'18

• A Language-Independent Approach to Smart Contract Verification

  Xiaohong Chen and Daejun Park and Grigore Rosu
  ISoLA'18 Springer, pp 405-413, November 2018
  PDF BIB ISoLA'18 Formally Verified Smart Contracts

• IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

  Theodoros Kasampalis and Dwight Guth and Brandon Moore and Traian Serbanuta and Virgil Serbanuta and Daniele Filaretti and Grigore Rosu and Ralph Johnson
  Technical Report July 2018 http://hdl.handle.net/2142/100320
  PDF BIB IELE

• Program Verification by Coinduction

  Brandon Moore and Lucas Pena and Grigore Rosu
  ESOP'18 Springer, pp 589-618, April 2018
  PDF BIB ESOP'18 Matching Logic

2017

• K - A Semantic Framework for Programming Languages and Formal Analysis Tools

  Grigore Rosu
  Marktoberdorf'16 {IOS} Press, 2017
  PDF BIB K

2016

• Semantics-Based Program Verifiers for All Languages

  Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
  OOPSLA'16 ACM, pp 74-91, Nov 2016
  PDF BIB OOPSLA'16 Matching Logic

• RV-Match: Practical Semantics-Based Program Analysis

  Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
  CAV'16 Springer, Volume 9779, pp 447-453, July 2016
  PDF BIB CAV'16 RV-Match

• A Language-Independent Proof System for Full Program Equivalence

  Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
  J.FAOC Volume 28, pp 469-497, May 2016
  PDF BIB J.FAOC Matching Logic

• Towards a Kool Future

  Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
  Boer's Festschrift Springer, Volume 9660, pp 325-343, January 2016
  PDF BIB Boer's Festschrift K

2015

• From Rewriting Logic, to Programming Language Semantics, to Program Verification

  Grigore Rosu
  Meseguer's Festschrift Springer, Volume 9200, pp 598-616, September 2015
  PDF BIB Meseguer's Festschrift K

• Matching Logic --- Extended Abstract

  Grigore Rosu
  RTA'15 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Volume 36, pp 5-21, July 2015
  PDF BIB RTA'15 Matching Logic

• KJS: A Complete Formal Semantics of JavaScript

  Daejun Park and Andrei Stefanescu and Grigore Rosu
  PLDI'15 ACM, pp 346-356, June 2015
  PDF BIB PLDI'15 Semantics

• Defining the Undefinedness of C

  Chris Hathhorn and Chucky Ellison and Grigore Rosu
  PLDI'15 ACM, pp 336-345, June 2015
  PDF BIB PLDI'15 C Semantics

• Term-Generic Logic

  Andrei Popescu and Grigore Rosu
  Journal of Theoretical Computer Science Volume 577, pp 1-24, April 2015
  PDF BIB Journal of Theoretical Computer Science

• Program Verification by Coinduction

  Brandon Moore and Grigore Rosu
  Technical Report February 2015 http://hdl.handle.net/2142/73177
  PDF BIB Matching Logic

• K-Java: A Complete Semantics of Java

  Denis Bogdanas and Grigore Rosu
  POPL'15 ACM, pp 445-456, January 2015
  PDF BIB POPL'15 K-Java

2014

• A Language-Independent Proof System for Mutual Program Equivalence

  Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
  ICFEM'14 Springer, Volume 8829, pp 75-90, November 2014
  PDF BIB ICFEM'14 Matching Logic

• Symbolic Analysis Tools for CSP

  Liyi Li and Elsa Gunter and William Mansky
  ICTAC'14 Springer International Publishing, pp 295-313, Sep 2014
  PDF BIB ICTAC'14 Holistic CSP

• All-Path Reachability Logic

  Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
  RTA'14 Springer, Volume 8560, pp 425-440, July 2014
  PDF BIB RTA'14 Matching Logic

• K Overview and SIMPLE Case Study

  Grigore Rosu and Traian Florin Serbanuta
  K'11 Elsevier, Volume 304, pp 3-56, June 2014
  PDF BIB K'11 K

• The K Primer (version 3.3)

  Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu
  K'11 Elsevier, Volume 304, pp 57-80, June 2014
  PDF BIB K'11 K

• Abstract Semantics for K Module Composition

  Codruta Girlea and Grigore Rosu
  K'11 Elsevier, Volume 304, pp 127-149, June 2014
  PDF BIB K'11 K

• On the Complexity of Stream Equality

  Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
  Journal of Functional Programming Volume 24, pp 166-217, May 2014
  PDF BIB Journal of Functional Programming CIRC

• Language Definitions as Rewrite Theories

  Andrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian Florin Serbanuta and Andrei Stefanescu and Grigore Rosu
  WRLA'14 Springer, Volume 8663, pp 97-112, April 2014
  PDF BIB WRLA'14 K

2013

• The Rewriting Logic Semantics Project: A Progress Report

  Jose Meseguer and Grigore Rosu
  Information and Computation Volume 231, pp 38-69, oct 2013
  PDF BIB Information and Computation K

• Specifying Languages and Verifying Programs with K

  Grigore Rosu
  SYNASC'13 IEEE, pp 28-31, September 2013
  PDF BIB SYNASC'13 K

• One-Path Reachability Logic

  Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
  LICS'13 IEEE, pp 358-367, June 2013
  PDF BIB LICS'13 Reachability Logic

• Low-Level Program Verification using Matching Logic Reachability

  Dwight Guth and Andrei Stefanescu and Grigore Rosu
  LOLA'13 , pp ---, June 2013
  PDF BIB LOLA'13 Matching Logic

2012

• Checking Reachability using Matching Logic

  Grigore Rosu and Andrei Stefanescu
  OOPSLA'12 ACM, pp 555-574, Oct 2012
  PDF BIB OOPSLA'12 Matching Logic

• From Hoare Logic to Matching Logic Reachability

  Grigore Rosu and Andrei Stefanescu
  FM'12 Springer, Volume 7436, pp 387-402, Aug 2012
  PDF BIB FM'12 Matching Logic

• Reachability Logic

  Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
  Technical Report Jul 2012 http://hdl.handle.net/2142/32952
  PDF BIB Reachability Logic

• Towards a Unified Theory of Operational and Axiomatic Semantics

  Grigore Rosu and Andrei Stefanescu
  ICALP'12 Springer, Volume 7392, pp 351-363, Jul 2012
  PDF BIB ICALP'12 Matching Logic

• An Executable Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  POPL'12 ACM, pp 533-544, January 2012
  PDF BIB POPL'12 Semantics

2011

• MatchC: A Matching Logic Reachability Verifier Using the K Framework

  Andrei Stefanescu
  K'11 Springer, Volume 304, August 2011
  PDF BIB Matching Logic

• The Rewriting Logic Semantics Project: A Progress Report

  Jose Meseguer and Grigore Rosu
  FCT'11 Springer, Volume 6914, pp 1-37, August 2011
  PDF BIB FCT'11 K

• An Executable Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  Technical Report July 2011 http://hdl.handle.net/2142/25816
  PDF BIB C Semantics

• Towards Semantics-Based WCET Analysis

  Mihail Asavoae and Dorel Lucanu and Grigore Rosu
  WCET'11 Austrian Computer Society, Volume , pp , July 2011
  PDF BIB WCET'11 Matching Logic

2010

• A Rewriting Approach to Concurrent Programming Language Design and Semantics

  Traian Florin Serbanuta
  PhD Thesis December 2010
  PDF BIB K

• Matching Logic: A New Program Verification Approach

  Grigore Rosu and Andrei Stefanescu
  UV'10 Nov 2010
  PDF BIB UV'10 Matching Logic

• A Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  Technical Report November 2010 http://hdl.handle.net/2142/17414
  PDF BIB C Semantics

2009

• Matching Logic --- Extended Report

  Grigore Rosu and Wolfram Schulte
  Technical Report January 2009 http://hdl.handle.net/2142/10790
  PDF BIB Matching Logic

2005

• Rewriting-Based Techniques for Runtime Verification

  Grigore Rosu and Klaus Havelund
  J.ASE Volume 12, pp 151-197, 2005
  PDF BIB J.ASE MOP

2004

• Composing Hidden Information Modules over Inclusive Institutions

  Joseph Goguen and Grigore Rosu
  Dahl's Festschrift Springer Berlin Heidelberg, Volume 2635, pp 96-123, September 2004
  PDF BIB Dahl's Festschrift

2003

• Certifying and Synthesizing Membership Equational Proofs

  Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer
  FME'03 Springer-Verlag, Volume 2805, pp 359-380, September 2003
  PDF BIB FME'03 Maude

2001

• Interpreting Abstract Interpretations in Membership Equational Logic

  Bernd Fischer and Grigore Rosu
  RULE'01 Elsevier, Volume 59(4), pp 271-285, June 2001
  PDF BIB Maude

• Certifying Domain-Specific Policies

  Michael Lowry and Thomas Pressburger and Grigore Rosu
  ASE'01 IEEE, pp 81-90, May 2001
  PDF BIB ASE'01 AutoFilter

• Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae

  Grigore Rosu and Klaus Havelund
  Technical Report January 2001 https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf
  PDF BIB

2000

• Abstract Semantics for Module Composition

  Grigore Rosu
  Technical Report May 2000 http://roger.ucsd.edu/record=b7304233~S9
  PDF BIB