Travelled to:1 × Austria
1 × United Kingdom
2 × France
6 × USA
Collaborated with:G.Rosu X.Qiu P.Madhusudan S.Ciobaca B.M.Moore D.Park T.Serbanuta P.Garg D.P.0001 Shijiao Yuwen Y.Li R.Mereuta A.Arusoaie D.Lucanu V.Rusu
Talks about:logic (6) reachabl (4) semant (3) match (3) structur (2) program (2) languag (2) theori (2) proof (2) path (2)
Person: Andrei Stefanescu
DBLP: Stefanescu:Andrei
Contributed to:
2015
2014
2014
20132013
2012
2012
2012
2012
20112016Wrote 11 papers:
- PLDI-2015-ParkSR #javascript #named #semantics
- KJS: a complete formal semantics of JavaScript (DP, AS, GR), pp. 346–356.
- RTA-TLCA-2014-StefanescuCMMSR #logic #reachability
- All-Path Reachability Logic (AS, SC, RM, BMM, TFS, GR), pp. 425–440.
- WRLA-2014-ArusoaieLRSSR
- Language Definitions as Rewrite Theories (AA, DL, VR, TFS, AS, GR), pp. 97–112.
- LICS-2013-RosuSCM #logic #reachability
- One-Path Reachability Logic (GR, AS, SC, BMM), pp. 358–367.
- PLDI-2013-Qiu0SM #proving
- Natural proofs for structure, data, and separation (XQ, PG, AS, PM), pp. 231–242.
- FM-2012-RosuS #hoare #logic #reachability
- From Hoare Logic to Matching Logic Reachability (GR, AS), pp. 387–402.
- ICALP-v2-2012-RosuS #axiom #formal method #semantics #towards
- Towards a Unified Theory of Operational and Axiomatic Semantics (GR, AS), pp. 351–363.
- OOPSLA-2012-RosuS #logic #reachability #using
- Checking reachability using matching logic (GR, AS), pp. 555–574.
- POPL-2012-MadhusudanQS #induction #proving #recursion
- Recursive proofs for inductive tree data-structures (PM, XQ, AS), pp. 123–136.
- ICSE-2011-RosuS #approach #logic #verification
- Matching logic: a new program verification approach (GR, AS), pp. 868–871.
- OOPSLA-2016-StefanescuPYLR #semantics #verification
- Semantics-based program verifiers for all languages (AS, DP0, SY, YL, GR), pp. 74–91.