Program Verification in the Presence of I/O.
Hugo Férée, Johannes Å. Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, [...]
Checking cryptographic API usage with composable annotations (short paper).
Duncan Mitchell, L. Thomas van Binsbergen, Blake Loring, and Johannes Kinder. PEPM ’18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, [...]
A B-tree library for Ocaml.
Tom Ridge. ICFP 2017. 2017
Logic in Computer ScienceOn the Quest for an Acyclic Graph.
Mikolas Janota, Radu Grigore, and Vasco Manquinho. arXiv: Logic in Computer Science. 2017
ExpoSE: practical symbolic execution of standalone JavaScript.
Blake Loring, Duncan Mitchell, and Johannes Kinder. SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, July 2017, [...]
Blockchain Superoptimizer.
Julian Nagele and Maria A Schett. Preproceedings of the 29th International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR 2019, 166-180. 2019
Implementing Multiparty Session Types in Rust.
Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. In: Bliudze, S., Bocchi, L. (eds) Coordination Models and Languages. COORDINATION 2020. Lecture Notes in Computer Science, vol [...]
Statically verified refinements for multiparty protocols.
Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA 2020, Article No.: [...]
Type checking beyond type checkers, via slice & run.
Justus Adam and Stephen Kell. TAPAS 2020: Proceedings of the 11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis, November 2020, 23–29. 2020
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.
Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. In: Gotsman, A., Sokolova, A. (eds) Formal Techniques for Distributed Objects, Components, [...]
by