Try-Mopsa: Relational Static Analysis in Your Pocket
Abstract elided by the publisher.
21,147 papers · page 22 of 1,058
Input-Based Three-Valued Abstraction Refinement
Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract s…
Efficient Discovery of Actual Causality in Stochastic Systems
Identifying the actual cause of events in engineered systems is a fundamental challenge in system analysis. Finding such causes becomes more challenging in the presence of noise and stochastic behavior in real-world systems. In this paper, we adopt the notion of probabilistic act…
Termination Resilience Static Analysis
Abstract elided by the publisher.
Verification of Generic VHDL Designs and Their Translation to Rocq
Abstract elided by the publisher.
Data Race Detection by Digest-Driven Abstract Interpretation
Abstract elided by the publisher.
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
Abstract elided by the publisher.
A Formal Executable Semantics of PROMELA
Abstract elided by the publisher.
Probabilistic Verification for Modular Network-on-Chip Systems
Abstract elided by the publisher.
Multi types and reasonable space
Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we …
Mixing visual and textual code
The dominant programming languages support nothing but linear text to express domain-specific geometric ideas. What is needed are hybrid languages that allow developers to create visual syntactic constructs so that they can express their ideas with a mix of textual and visual syn…
Don't exhaust, don't waste: Resource-aware soundness for big-step semantics
We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, and is stuck, besides in case of type errors, if either a needed resource is exhausted, or a provided…
A simple and efficient implementation of strong call by need by an abstract machine
Strong call-by-need combines full normalization with the sharing discipline of lazy evaluation, yet no prior implementation achieved both simplicity and efficiency. We introduce RKNL, an abstract machine that realizes strong call-by-need with bilinear overhead. The machine has be…
Types, equations, dimensions and the Pi theorem
The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We ap…
Adapting the MVVM pattern to C++ frontends and Agda-based backends
Using agda2hs and ad-hoc Haskell FFI bindings, writing Qt applications in C++ with Agda- or Haskell-based backends (possibly including correctness proofs) is already possible. However, there was no repeatable methodology to do so, nor to use arbitrary Haskell built-in libraries i…
Longest r-chain: thinning by grouping
r ⊆ s⇒ length (longest-chain r xs) ⩽ length (longest-chain s xs).If we set the distance to, say, 13, then the poem is almost completely uncovered.> longest-chain (close 13) .unlines .take 2 .lines .
Proto-Quipper with dynamic lifting
Quipper is a functional language for programming quantum circuits. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting, which is present in Quipper. By virtue of…
Higher-order bialgebraic semantics
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality resu…
Etna: An evaluation platform for property-based testing
Property-based testing is a mainstay of functional programming, boasting a rich literature, an enthusiastic user community, and an abundance of tools~ -- so many, indeed, that new users may have difficulty choosing. Moreover, any given framework may support a variety of strategie…
Modular models of monoids with operations by lifting functors along fibrations
Inspired by Plotkin and Power's algebraic treatment of computational effects and the principle of notions of computations as monoids, we propose a categorical framework for equational theories and models of monoids equipped with operations. This framework generalises Plotkin and …