February 25, 2013
My first PC membership
! FCS 2013 !
! Workshop on Foundations of Computer Security !
! Tulane University, New Orleans, Louisiana, USA !
! June 29, 2013 !
! http://prosecco.inria.fr/personal/bblanche/fcs13/ !
! Affiliated with LICS 2013 and CSF 2013 !
Submission: April 10, 2013
Notification of acceptance: April 30, 2013
Final papers: May 31, 2013
Invited speaker: Boris Koepf, IMDEA, Spain
Read the rest of this entry »
February 16, 2013
Our paper marrying reliable exception handling and sound fine-grained dynamic information flow control was accepted at the IEEE Symposium on Security & Privacy (Oakland 2013).
All Your IFCException Are Belong To Us. Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett.
December 23, 2012
This semester Benjamin Pierce gave a course on Advanced Coq Martial Arts based on Adam Chlipala’s CPDT book. The course was very interactive, with the students giving most of the lectures and being in charge of creating the exercises. Since I wanted to know more about coinduction I taught the coinduction lectures and learned a lot in the process. One of the results of these lectures is a new set of materials for teaching coinduction in Coq:
These materials are based on Adam’s book chapter, Giménez and Castéran’s tutorial, and Xavier Leroy and Herve Grall’s development on coinductive operational semantics. I’ve tried my best to explain things better and to add good exercises.
Another result is a new Coq tactic that allows for aggressive automation of coinductive proofs. Most of the easy proofs now take the form coind using coind_principle; crush.
Read the rest of this entry »
July 11, 2011
The “Alexandru Ioan Cuza” University from Iaşi scored second in the 2011 Computer Science scientific results ranking:
- Universitatea Babeş-Bolyai, Cluj Napoca
- Universitatea Alexandru Ioan Cuza, Iaşi
- Universitatea Valahia, Târgovişte
- Universitatea Bucureşti, Bucureşti
- Universitatea Politehnica Bucureşti
As always take this ranking with a big grain of salt.
May 13, 2011
Alex Busenius and me are pleased to announce that Expi2Java 1.6 was released two days ago. And by the way, Alex has recently finished his MSc and is looking for a job in industry. If you know anything interesting in a German or English speaking country, please let him know.
Expi2Java 1.6 was released yesterday (11.05.2011)
The highlights of this release are the new symbolic library and a mechanized formalization in Coq.
The symbolic library abstracts away cryptographic primitives as symbolic terms and networking as pi-calculus-like channels. It is designed to be sound and simple enough to simplify proving the transformation secure. Both the symbolic and concrete libraries can be used interchangeably with all provided examples.
We have formalized the transformation from Expi Calculus to a subset of Java performed by Expi2Java using the Coq proof assistant and proved the symbolic library and the produced Java code to be well-typed. The formalization and all proofs can be found on the project homepage.
The full list of changes: Read the rest of this entry »
November 11, 2010
The ICFP 2010 talks are online for some days … hours and hours of home entertainment! Here is the presentation of my favorite ICFP 2010 paper:
And here is my own stressed and tired talk (for a less stressed version see this):
It’s amazing how much you can learn from a video of your own talk. So many times your impression as a speaker about what the audience got out of your talk are completely off. I wish more conferences would record talks, then maybe the talks would get better.
September 23, 2010
DVerify is a new tool for verifying Dminor programs. It achieves pretty much the same thing as the Dminor type-checker, just in a quite different way: DVerify translates Dminor programs into a quite standard while language, and then uses the Boogie generic verification condition generator backend to verify the translated program. The soundness of this technique has been proved formally using Coq. DVerify and the Coq proofs are the product of Thorsten Tarrach’s recently defended Master’s thesis.
September 20, 2010
Today we released version 0.1.1 of Dminor, our type-checker for a subset of the code name “M” Modeling Language. This brings several bug fixes and a couple of optimizations to our semantic-subtyping-based prototype type-checker. Andy Gordon posted about the original release of Dminor in December.
September 8, 2010
“Computational functions are reflected, at the logical level, as pairs of a precondition and postcondition. [...] A function’s precondition and postcondition alone determine how it is lifted: its code is ignored. (The conformance of a function’s body to its declared pre- and postcondition
is checked, of course, via a proof obligation [...]) This reflects a philosophy in which the only way of reasoning about the behavior of a function value is via its specification: code never appears within formulae.” — It seems that it took a very long time until this extremely natural idea was finally incorporated in a decent Hoare logic for functional programs (and a couple more years until it finally reached the world of refinement type systems )
“In this paper, we [...] allow specifications to be expressed in higher-order logic. The intuitive justification for this approach is that, if functions can abstract over functions, then specifications must abstract over specifications.”