Travelled to:1 × France
1 × Hungary
1 × India
1 × Ireland
1 × Japan
1 × Spain
1 × Sweden
1 × Switzerland
2 × Italy
3 × Germany
4 × United Kingdom
8 × USA
Collaborated with:D.Devriese B.Jacobs J.Smans D.Vanoverberghe B.Reynders J.Cockx M.Patrignani W.Schulte I.Sergey D.Clarke P.Müller W.Penninckx P.Agten F.Vogels N.Tillmann A.Moors M.Odersky K.R.M.Leino M.Ngo F.Massacci D.Milushev P.D.Ryck L.Desmet W.Joosen T.Winant T.Schrijvers M.Dam A.Lundblad J.T.Mühlberg D.H.White M.Dodds G.Lüttgen M.Denecker K.V.Belleghem G.Duchatelet D.D.Schreye M.Might J.Midtgaard D.Darais V.Klebanov N.Shankar G.T.Leavens V.Wüstholz E.Alkassar R.Arthan D.Bronish R.Chapman E.Cohen M.A.Hillebrand R.Monahan N.Polikarpova T.Ridge S.Tobies T.Tuerk M.Ulbrich B.Weiß
Talks about:program (7) type (5) verif (4) sound (4) modular (3) generat (3) verifi (3) frame (3) dynam (3) safe (3)
Person: Frank Piessens
DBLP: Piessens:Frank
Contributed to:
2015
2015
2015
2015
20152014
2014
2014
20142013
2013
2013
2011
20112011201120112010
2009
20092008
200820072005
199620162018Wrote 31 papers:
- ESOP-2015-Penninckx0P #behaviour #composition #source code #verification
- Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs (WP, BJ, FP), pp. 158–182.
- GPCE-2015-ReyndersDP #api #bound #generative
- Generating safe boundary APIs between typed EDSLs and their environments (BR, DD, FP), pp. 31–34.
- POPL-2015-Agten0P #c #composition #verification
- Sound Modular Verification of C Code Executing in an Unverified Context (PA, BJ, FP), pp. 581–594.
- POPL-2015-NgoMMP #black box #policy #runtime #security #source code
- Runtime Enforcement of Security Policies on Black Box Reactive Programs (MN, FM, DM, FP), pp. 43–54.
- SAC-2015-RyckDPJ #named
- SecSess: keeping your session tucked away in your browser (PDR, LD, FP, WJ), pp. 2171–2176.
- SEFM-2015-Muhlberg0DLP #learning #source code #verification
- Learning Assertions to Verify Linked-List Programs (JTM, DHW, MD, GL, FP), pp. 37–52.
- ESOP-2014-CockxPD #independence #similarity
- Overlapping and Order-Independent Patterns — Definitional Equality for All (JC, FP, DD), pp. 87–106.
- ICFP-2014-CockxDP #pattern matching
- Pattern matching without K (JC, DD, FP), pp. 257–268.
- Onward-2014-ReyndersDP #functional #multi #programming #web
- Multi-Tier Functional Reactive Programming for the Web (BR, DD, FP), pp. 55–68.
- PADL-2014-WinantDPS #haskell
- Partial Type Signatures for Haskell (TW, DD, FP, TS), pp. 17–32.
- ICFP-2013-DevrieseP #metaprogramming
- Typed syntactic meta-programming (DD, FP), pp. 73–86.
- PEPM-2013-DevrieseSCP #domain-specific language #recursion
- Fixing idioms: a recursion primitive for applicative DSLs (DD, IS, DC, FP), pp. 97–106.
- PLDI-2013-SergeyDMMDCP #monad
- Monadic abstract interpreters (IS, DD, MM, JM, DD, DC, FP), pp. 399–410.
- FASE-2011-VanoverbergheP #aspect-oriented #composition #execution #symbolic computation
- Theoretical Aspects of Compositional Symbolic Execution (DV, FP), pp. 247–261.
- FM-2011-JacobsSP #verification
- Verification of Unloadable Modules (BJ, JS, FP), pp. 402–416.
- FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
- The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
- ICFP-2011-DevrieseP #on the
- On the bright side of type classes: instance arguments in Agda (DD, FP), pp. 143–155.
- PADL-2011-DevrieseP #combinator #domain-specific language #recursion #semiparsing
- Explicitly Recursive Grammar Combinators — A Better Model for Shallow Parser DSLs (DD, FP), pp. 84–98.
- POPL-2011-JacobsP #composition #concurrent #fine-grained #specification
- Expressive modular fine-grained concurrency specification (BJ, FP), pp. 271–282.
- SAC-2010-VogelsJP #generative #performance #proving #verification
- A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
- ECOOP-2009-DamJLP #java #monitoring #parallel #security #thread
- Security Monitor Inlining for Multithreaded Java (MD, BJ, AL, FP), pp. 546–569.
- ECOOP-2009-JacobsP #exception #named
- Failboxes: Provably Safe Exception Handling (BJ, FP), pp. 470–494.
- ECOOP-2009-SmansJP #logic
- Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic (JS, BJ, FP), pp. 148–172.
- TACAS-2009-VanoverbergheTP #generative #pointer #source code
- Test Input Generation for Programs with Pointers (DV, NT, FP), pp. 277–291.
- FASE-2008-SmansJPS #automation #java #source code #verification
- An Automatic Verifier for Java-Like Programs Based on Dynamic Frames (JS, BJ, FP, WS), pp. 261–275.
- OOPSLA-2008-MoorsPO
- Generics of a higher kind (AM, FP, MO), pp. 423–438.
- SEFM-2007-JacobsMP #exception #reasoning
- Sound reasoning about unchecked exceptions (BJ, PM, FP), pp. 113–122.
- SEFM-2005-JacobsPLS #concurrent #invariant
- Safe Concurrency for Aggregate Objects with Invariants (BJ, FP, KRML, WS), pp. 137–147.
- JICSLP-1996-DeneckerBDPS #calculus #empirical #information management #protocol #representation #specification
- A Realistic Experiment in Knowledge Representation in Open Event Calculus: Protocol Specification (MD, KVB, GD, FP, DDS), pp. 170–184.
- POPL-2016-DevriesePP #approximate #compilation
- Fully-abstract compilation by approximate back-translation (DD, MP, FP), pp. 164–177.
- POPL-2018-DevriesePP #parametricity
- Parametricity versus the universal type (DD, MP, FP), p. 23.