Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps
Abstract elided by the publisher.
613 papers · page 6 of 31
Pumping, with or Without Choice
Abstract elided by the publisher.
On Strings in Software Model Checking
Abstract elided by the publisher.
Succinct Determinisation of Counting Automata via Sphere Construction
We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the naive approach, and thus produces much smaller deterministic automata. We als…
A Type-Based HFL Model Checking Algorithm
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem…
A Dependently Typed Multi-stage Calculus
We study a dependently typed extension of a multi-stage programming language a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct for execution of programs dynamically gener…
Mimalloc: Free List Sharding in Action
Abstract elided by the publisher.
Proving that Programs Are Differentially Private
Abstract elided by the publisher.
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
Abstract elided by the publisher.
Recursion Schemes in Coq
Abstract elided by the publisher.
Reducing Static Analysis Alarms Based on Non-impacting Control Dependencies
Abstract elided by the publisher.
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific lan…
Manifest Contracts with Intersection Types
We present a manifest contract system PCFv$\Delta$H with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a refinement type system and consistency of contracts is checked by combination of compile- and r…
Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning
Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in th…
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
Abstract elided by the publisher.
Uniform Random Process Model Revisited
Abstract elided by the publisher.
The Practice of a Compositional Functional Programming Language
Abstract elided by the publisher.
Types of Fireballs
Abstract elided by the publisher.
Scallina: Translating Verified Programs from Coq to Scala
Abstract elided by the publisher.
Factoring Derivation Spaces via Intersection Types
Abstract elided by the publisher.