Programming Language Design and Semantics

2019

• SETSS’19 Lecture Notes on K
  Chen, Xiaohong and Rosu, Grigore.
  SETSS’19 Springer, pp .
  2019
  PDF BIB
• A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
  Dasgupta, Sandeep and Park, Daejun and Kasampalis, Theodoros and Adve, Vikram S. and Roşu, Grigore.
  PLDI’19 ACM, pp 1133-1148.
  2019
  PDF BIB

2018

• Program Verification by Coinduction
  Moore, Brandon and Peña, Lucas and Roşu, Grigore.
  ESOP’18 Springer, pp 589-618.
  2018
  PDF BIB
• A Language-Independent Approach to Smart Contract Verification
  Chen, Xiaohong and Park, Daejun and Roşu, Grigore.
  ISoLA’18 Springer, pp 405-413.
  2018
  PDF BIB
• IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
  Kasampalis, Theodoros and Guth, Dwight and Moore, Brandon and Serbanuta, Traian and Serbanuta, Virgil and Filaretti, Daniele and Rosu, Grigore and Johnson, Ralph.
  2018
  PDF BIB
• A Language-Independent Program Verification Framework
  Chen, Xiaohong and Roşu, Grigore.
  ISoLA’18 Springer, pp 92-102.
  2018
  PDF BIB

2017

• K - A Semantic Framework for Programming Languages and Formal Analysis Tools
  Rosu, Grigore.
  Marktoberdorf’16 IOS Press, pp .
  2017
  PDF BIB

2016

• A Language-Independent Proof System for Full Program Equivalence
  Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore.
  2016
  PDF BIB
• RV-Match: Practical Semantics-Based Program Analysis
  Guth, Dwight and Hathhorn, Chris and Saxena, Manasvi and Rosu, Grigore.
  CAV’16 Springer, pp 447-453.
  2016
  PDF BIB
• Towards a Kool Future
  Lucanu, Dorel and Şerbănuţă, Traian Florin and Roşu, Grigore.
  Boer’s Festschrift Springer, pp 325-343.
  2016
  PDF BIB
• Semantics-Based Program Verifiers for All Languages
  Ştefănescu, Andrei and Park, Daejun and Yuwen, Shijiao and Li, Yilong and Roşu, Grigore.
  OOPSLA’16 ACM, pp 74-91.
  2016
  PDF BIB

2015

• Program Verification by Coinduction
  Moore, Brandon and Roşu, Grigore.
  2015
  PDF BIB
• From Rewriting Logic, to Programming Language Semantics, to Program Verification
  Roşu, Grigore.
  Meseguer’s Festschrift Springer, pp 598-616.
  2015
  PDF BIB
• Term-Generic Logic
  Popescu, Andrei and Roşu, Grigore.
  2015
  PDF BIB
• K-Java: A Complete Semantics of Java
  Bogdănaş, Denis and Roşu, Grigore.
  POPL’15 ACM, pp 445-456.
  2015
  PDF BIB
• Defining the Undefinedness of C
  Hathhorn, Chris and Ellison, Chucky and Roşu, Grigore.
  PLDI’15 ACM, pp 336-345.
  2015
  PDF BIB
• KJS: A Complete Formal Semantics of JavaScript
  Park, Daejun and Ştefănescu, Andrei and Roşu, Grigore.
  PLDI’15 ACM, pp 346-356.
  2015
  PDF BIB
• Matching Logic — Extended Abstract
  Roşu, Grigore.
  RTA’15 Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp 5-21.
  2015
  PDF BIB

2014

• A Language-Independent Proof System for Mutual Program Equivalence
  Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore.
  ICFEM’14 Springer, pp 75-90.
  2014
  PDF BIB
• K Overview and SIMPLE Case Study
  Rosu, Grigore and Serbanuta, Traian Florin.
  K’11 Elsevier, pp 3-56.
  2014
  PDF BIB
• Symbolic Analysis Tools for CSP
  Li, Liyi and Gunter, Elsa and Mansky, William.
  ICTAC’14 Springer International Publishing, pp 295-313.
  2014
  PDF BIB
• Abstract Semantics for K Module Composition
  Girlea, Codruta and Rosu, Grigore.
  K’11 Elsevier, pp 127-149.
  2014
  PDF BIB
• Language Definitions as Rewrite Theories
  Arusoaie, Andrei and Lucanu, Dorel and Rusu, Vald and Şerbănuţă, Traian Florin and Ştefănescu, Andrei and Roşu, Grigore.
  WRLA’14 Springer, pp 97-112.
  2014
  PDF BIB
• All-Path Reachability Logic
  Ştefănescu, Andrei and Ştefan Ciobâcă and Mereuţă, Radu and Moore, Brandon M. and Şerbănuţă, Traian Florin and Roşu, Grigore.
  RTA’14 Springer, pp 425-440.
  2014
  PDF BIB
• On the Complexity of Stream Equality
  Endrullis, Jörg and Hendriks, Dimitri and Bakhshi, Rena and Roşu, Grigore.
  2014
  PDF BIB
• The K Primer (version 3.3)
  Serbanuta, Traian Florin and Arusoaie, Andrei and Lazar, David and Ellison, Chucky and Lucanu, Dorel and Rosu, Grigore.
  K’11 Elsevier, pp 57-80.
  2014
  PDF BIB

2013

• One-Path Reachability Logic
  Roşu, Grigore and Ştefănescu, Andrei and Ştefan Ciobâcă and Moore, Brandon M..
  LICS’13 IEEE, pp 358-367.
  2013
  PDF BIB
• Specifying Languages and Verifying Programs with K
  Rosu, Grigore.
  SYNASC’13 IEEE, pp 28-31.
  2013
  PDF BIB
• Low-Level Program Verification using Matching Logic Reachability
  Guth, Dwight and Ştefănescu, Andrei and Roşu, Grigore.
  LOLA’13 , pp —.
  2013
  PDF BIB
• The Rewriting Logic Semantics Project: A Progress Report
  Meseguer, José and Roşu, Grigore.
  2013
  PDF BIB

2012

• An Executable Formal Semantics of C with Applications
  Ellison, Chucky and Rosu, Grigore.
  POPL’12 ACM, pp 533-544.
  2012
  PDF BIB
• Towards a Unified Theory of Operational and Axiomatic Semantics
  Roşu, Grigore and Ştefănescu, Andrei.
  ICALP’12 Springer, pp 351-363.
  2012
  PDF BIB
• From Hoare Logic to Matching Logic Reachability
  Roşu, Grigore and Ştefănescu, Andrei.
  FM’12 Springer, pp 387-402.
  2012
  PDF BIB
• Reachability Logic
  Roşu, Grigore and Ştefănescu, Andrei and Ştefan Ciobâcă and Moore, Brandon M..
  2012
  PDF BIB
• Checking Reachability using Matching Logic
  Roşu, Grigore and Ştefănescu, Andrei.
  OOPSLA’12 ACM, pp 555-574.
  2012
  PDF BIB

2011

• An Executable Formal Semantics of C with Applications
  Ellison, Chucky and Roşu, Grigore.
  2011
  PDF BIB
• Towards Semantics-Based WCET Analysis
  Asavoae, Mihail and Lucanu, Dorel and Rosu, Grigore.
  WCET’11 Austrian Computer Society, pp .
  2011
  PDF BIB
• MatchC: A Matching Logic Reachability Verifier Using the K Framework
  Ştefănescu, Andrei.
  K’11 Springer, pp .
  2011
  PDF BIB
• The Rewriting Logic Semantics Project: A Progress Report
  Meseguer, José and Roşu, Grigore.
  FCT’11 Springer, pp 1-37.
  2011
  PDF BIB

2010

• A Formal Semantics of C with Applications
  Ellison, Chucky and Roşu, Grigore.
  2010
  PDF BIB
• A Rewriting Approach to Concurrent Programming Language Design and Semantics
  Şerbănuţă, Traian Florin.
  2010
  PDF BIB
• Matching Logic: A New Program Verification Approach
  Roşu, Grigore and Ştefănescu, Andrei.
  UV’10 , pp .
  2010
  PDF BIB

2009

• Matching Logic — Extended Report
  Rosu, Grigore and Schulte, Wolfram.
  2009
  PDF BIB

2005

• Rewriting-Based Techniques for Runtime Verification
  Rosu, Grigore and Havelund, Klaus.
  2005
  PDF BIB

2004

• Composing Hidden Information Modules over Inclusive Institutions
  Goguen, Joseph and Rosu, Grigore.
  Dahl’s Festschrift Springer Berlin Heidelberg, pp 96-123.
  2004
  PDF BIB

2003

• Certifying and Synthesizing Membership Equational Proofs
  Rosu, Grigore and Eker, Steven and Lincoln, Patrick and Meseguer, Jose.
  FME’03 Springer-Verlag, pp 359-380.
  2003
  PDF BIB

2001

• Certifying Domain-Specific Policies
  Lowry, Michael and Pressburger, Thomas and Rosu, Grigore.
  ASE’01 IEEE, pp 81-90.
  2001
  PDF BIB
• Interpreting Abstract Interpretations in Membership Equational Logic
  Fischer, Bernd and Rosu, Grigore.
  RULE’01 Elsevier, pp 271-285.
  2001
  PDF BIB
• Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae
  Rosu, Grigore and Havelund, Klaus.
  2001
  PDF BIB

2000

• Abstract Semantics for Module Composition
  Rosu, Grigore.
  2000
  PDF BIB