#formal verification
43 papers · 1 filter
Formalization of security
Gilles Barthe
The paper discusses how proof assistants can be used to formally verify security properties of systems, languages, compilers, and cryptographic protocols, supporting certification…
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
Pablo Manrique, Stefan Szeider
The paper presents LeanCSP, a framework built in the Lean theorem prover that can formally verify constraint reformulations and certify solver results for constraint problems, prov…
Checking Information Flow in Cloud-based IoT Access Control Policies (Extended Version)
Lorenzo Ceragioli, Letterio Galletta, Edoardo Lunati
The paper presents a method to detect unwanted information flow in cloud‑based IoT access control policies by modeling AWS IoT Core components and using an SMT‑based analysis tool…
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
Shuo Deng, Kenneth W. Shum
The paper describes an ongoing effort to formalize a university-level probability textbook in the Lean theorem prover, creating a machine‑checked companion and reusable probability…
Deductive Verification for Earliest Deadline First Scheduler Implementations
Daniel Kuhse, Junjie Shi, Jan Duy Thien Pham +4
The paper formalizes correctness criteria for Earliest Deadline First (EDF) schedulers and presents a deductive verification framework, demonstrated on EDF implementations in RTEMS…
Property-driven Causal Abstractions for Markov Decision Processes
Jule Schmidt, Maximilian Weininger, Clemens Dubslaff +2
The paper proposes a property-driven causal abstraction method for factored Markov Decision Processes that groups states sharing the same causal reasons for satisfying or violating…