We develop a denotational model for probabilistic and concurrent imperative programs , a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas the semantics of concurrent programs and of randomized programs are each well studied in isolation, their combination remains poorly understood. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution are not captured by straightforward generalizations of pomsets or convex languages—the prominent models for each effect on its own. Our work introduces the first denotational model for probabilistic concurrent programs with unbounded looping, a major step towards verification of these programs. We prove that the model has good domain-theoretic properties, important for semantics of unbounded loops, as well as two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism. We illustrate the reasoning power of the new model with an analysis of the randomized solution to Dijkstra's Dining Philosophers problem, adapted from Lehmann and Rabin.
We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiments, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We collect and analyse over 1,700 student submissions to 11 programming exercises and show how our grader can prove submission correctness and report counterexamples. Beyond functional correctness, we were able to use the outcome of equivalence checks to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input–output behaviour is identical. Consequently, we achieve (1) higher confidence in correctness of idiomatic solutions but also (2) more thorough assessment of solution landscape that reveals solutions beyond those envisioned by instructors.
Compiling a high-level functional programming language to machine code that can be executed efficiently on a modern machine is complicated, since we have to traverse many different levels of abstraction. This is particularly challenging if the language contains some form of control effects and a mix of different evaluation strategies, such as call-by-value data types and call-by-name codata types. In this paper, we tell the complete story, starting from a simple functional programming language with control effects and both data and codata types, and ending up with machine code for standard platforms. What distinguishes our compiler from all other existing compilers for functional programming languages is that, instead of natural-deduction-based languages like the lambda calculus, we use sequent-calculus-inspired languages throughout all intermediate stages. These sequent-calculus-based languages are characterized by the first-class nature of consumers, which represent program contexts. In this sense, we view our work as a continuation, and generalization, of Andrew Appel's landmark work on “Compiling with Continuations”.
Over the past decades, context sensitivity has been considered key to improving the precision of whole-program pointer analysis for object-oriented languages such as Java. By analyzing a method under distinct contexts, it separates the static representations of different dynamic instantiations of variables and heap objects, thereby reducing spurious object flows. However, despite its precision benefits, context sensitivity incurs substantial efficiency costs because each method is analyzed multiple times under different contexts. To mitigate this issue, numerous selective context-sensitive approaches have been proposed that apply context sensitivity only to selected methods. However, these approaches do not fully eliminate the efficiency bottleneck because they still rely on the fundamental idea of context sensitivity—analyzing a method multiple times based on calling contexts—which limits scalability on large programs. In this work, we propose Cut-Shortcut , a fundamentally different approach for fast yet precise Java pointer analysis. The core insight is that the primary benefit of context sensitivity is to filter spurious object flows merged within callee methods; from the perspective of a pointer flow graph, this effect can be obtained without explicit contexts by suppressing the addition of imprecise flow edges ( Cut ) and adding Shortcut edges that directly connect source pointers to target pointers across method boundaries. This insight is distilled into a general principle and instantiated via three well-characterized program patterns under which suppressing imprecise flows and adding precise shortcut flows are provably safe. We formalize Cut-Shortcut via inference rules and prove soundness. A context-free-language (CFL) reachability formulation is further provided to relate Cut-Shortcut to well-understood formal models of pointer analysis and to show that Cut-Shortcut has the same worst-case asymptotic complexity as context-insensitive analysis. To address new sources of imprecision introduced in modern Java, we further propose Cut-Shortcut \({}^{\mathcal{S}}\) , extending one of the patterns to handle Streams and their interaction with Lambda Expressions by distinguishing flows across different stream pipelines. Implemented in the state-of-the-art pointer analysis framework Tai-e , Cut-Shortcut is evaluated on 10 large, complex Java programs from recent literature, and Cut-Shortcut \({}^{\mathcal{S}}\) is evaluated on three new stream-heavy benchmark suites that we created (with 20 programs in total). Results show that Cut-Shortcut achieves precision close to (selective) context-sensitive analysis (where applicable), while being faster than context-insensitive analysis on 9 of the 10 programs and matching it on the remaining one. Moreover, Cut-Shortcut \({}^{\mathcal{S}}\) yields substantial precision improvement while preserving scalability and efficiency for programs with heavy stream usage. To the best of our knowledge, this work is the first to achieve such a good efficiency-precision tradeoff for hard-to-analyze Java programs, including large-scale and feature-rich applications.
Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.
