6 citations · 17 across the 6 of their papers we have counts for
7 papers
Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
Li-yao Xia, Laura Israel, Maite Kramarz +4
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computati…
QuickerCheck: Implementing and Evaluating a Parallel Run-Time for QuickCheck
Robert Krook, Nicholas Smallbone, Bo Joel Svensson +1
This paper introduces a new parallel run-time for QuickCheck, a Haskell library and EDSL for specifying and randomly testing properties of programs. The new run-time can run multip…
HasTEE: Programming Trusted Execution Environments with Haskell
Abhiroop Sarkar, Robert Krook, Alejandro Russo +1
Trusted Execution Environments (TEEs) are hardware-enforced memory isolation units, emerging as a pivotal security solution for security-critical applications. TEEs, like Intel SGX…
Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans
Johan Lidén Eddeland, Koen Claessen, Nicholas Smallbone +3
Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuo…
A Supervisory Control Algorithm Based on Property-Directed Reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovács +1
We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The…
Hipster: Integrating Theory Exploration in a Proof Assistant
Moa Johansson, Dan Rosen, Nicholas Smallbone +1
This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new int…
A Faithful Semantics for Generalised Symbolic Trajectory Evaluation
Koen Claessen, Jan-Willem Roorda
Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formal verification technique for hardware. GSTE uses abstraction, meaning that details of the circuit behaviou…