Search events for 'all'
How to secure a distributed database such as OpenRiak with open-source tools
Tutorials People: Nicholas Adams, Peter Clark
… For ease of use, many pieces of software are insecure in their default settings. Not realising this, users in all the major categories - academic, industry and hobbyist, will often run said software in a configuration where vulnerabilities …
Concurrent Algorithms under the hood of Kotlin Coroutines
Tutorials People: Nikita Koval
… the Lincheck framework designed to test all … the problems we have faced when improving Kotlin Coroutines, present all …
Testing concurrent code on JVM with Lincheck
Tutorials People: Evgenii Moiseenko, Nikita Koval
… in the Java standard library. All tasks run locally on attendees’ laptops. By the end …
Automating maintenance of the Linux kernel: a perspective over 20 years
SPLASH Keynotes People: Julia Lawall
… in thousands of kernel commits. However, not all software issues can be neatly …
Software Stacks for Confidential Computing Hardware
SPLASH Keynotes People: Frank Piessens
… is rapidly gaining traction in industry. All major hardware vendors have …
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
ICFP Papers People: Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
… examples and larger case studies. All of the presented results, including the meta …
Reasoning about Weak Isolation Levels in Separation Logic
ICFP Papers People: Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal
… effort of the database serves as proof that all of our specifications are realizable. All results are mechanized in the Rocq proof assistant on top of the Iris …
Multi-Stage Programming with Splice Variables
ICFP Papers People: Tsung-Ju Chiang, Ningning Xie
… using a Kripke-style model, and prove adequacy results. All proofs have been fully …
Type Theory in Type Theory Using a Strictified Syntax
ICFP Papers People: Ambrus Kaposi, Loïc Pujet
… as metatheoretical functions. This has the effect of strictifying all the equations …
Almost Fair Simulations
ICFP Papers People: Arthur Correnson, Iona Kuhn, Bernd Finkbeiner
… "uchi fairness condition. The simulation relations we present can all be equipped …
Robust Dynamic Embedding for Gradual Typing
ICFP Papers People: Koen Jacobs, Matías Toro, Nicolas Tabareau, Éric Tanter
… language. All the results are formalized in the Rocq proof assistant. This novel …
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
ICFP Papers People: Rutger Broekhoff, Robbert Krebbers
… based on deferred substitutions.
We mechanize all our results in the Rocq prover …