FM 2019: 23RD INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

A
Aichernig, Bernhard K.	L*-Based Learning of Markov Decision Processes
Amram, Gal	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
Andronick, June	Successes in Deployed Verified Software (and Insights on Key Social Factors)
Appel, Andrew W.	Abstraction and Subsumption in Modular Verification of C Programs
Arusoaie, Andrei	Unification in Matching Logic
B
Bacci, Giovanni	L*-Based Learning of Markov Decision Processes
Baier, Christel	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Bao, Yuyan	Unifying separation logic and region logic to allow interoperability
Bard, Joachim	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
Becker, Heiko	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
Bendisposto, Jens	Embedding High-Level Formal Specifications into Applications
Beringer, Lennart	Abstraction and Subsumption in Modular Verification of C Programs
Blakqori, Genc	APML: An Architecture Proof Modelling Language
Bodeveix, Jean-Paul	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Bonakdarpour, Borzoo	Gray-Box Monitoring of Hyperproperties
Bonsangue, Marcello	On the Nature of Symbolic Execution
Boyer, Benoît	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Brenas, Jon Haël	Reasoning Formally about Database Queries and Updates
Brunel, Julien	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Butterfield, Andrew	Towards a Model-Checker for Circus Circus2CSP: A Tool for Model-Checking Circus Using FDR
C
Charguéraud, Arthur	GOSPEL - Providing OCaml with a Formal Specification Language
Chemouil, David	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Cordwell, Katherine	Pegasus: A Framework for Sound Continuous Invariant Generation
Coughlin, Nicholas	Value-Dependent Information-Flow Security on Weak Memory Models
D
D'Souza, Deepak	Static Analysis for Detecting High-Level Races in RTOS Kernels
D'Souza, Meenakshi	Static Analysis for Detecting High-Level Races in RTOS Kernels
Darulova, Eva	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
de Boer, Frank S.	On the Nature of Symbolic Execution
Dehnert, Christian	Counterexample-Driven Synthesis for Probabilistic Program Sketches
Deifel, Hans-Peter	Generic Partition Refinement and Weighted Tree Automata
Derrick, John	Verifying Correctness of Persistent Concurrent Data Structures
Doherty, Simon	Verifying Correctness of Persistent Concurrent Data Structures
Dongol, Brijesh	Verifying Correctness of Persistent Concurrent Data Structures
Dubrulle, Paul	Local Consistency Check in Synchronous Dataflow Models
Dunkelau, Jannik	Embedding High-Level Formal Specifications into Applications
E
Echahed, Rachid	Reasoning Formally about Database Queries and Updates
Ehlers, Rüdiger	How Hard is Finding Shortest Counter-Example Lassos in Model Checking?
Eichlseder, Maria	L*-Based Learning of Markov Decision Processes
Ernst, Gidon	Unifying separation logic and region logic to allow interoperability
Evangelidis, Alexandros	Quantitative Verification of Numerical Stability for Kalman Filters
F
Feliú, Marco A.	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Filali, Mamoun	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Filaretti, Daniele	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Filliâtre, Jean-Christophe	GOSPEL - Providing OCaml with a Formal Specification Language
G
Gomes, Artur Oliveira	Towards a Model-Checker for Circus Circus2CSP: A Tool for Model-Checking Circus Using FDR
Guth, Dwight	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
H
H. Pham, Long	Concolic Testing Heap-Manipulating Programs
Hähnle, Reiner	Abstract Execution
I
Irofti, Dina	Local Consistency Check in Synchronous Dataflow Models
J
Jackson, Daniel	Alloy*: a general-purpose higher-order relational constraint solver
Jantsch, Simon	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Johansen, Christian	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Johnson, Ralph	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Johnson, Taylor T.	Star-Based Reachability Analysis of Deep Neural Networks
Jongmans, Sung-Shik	SOA and the Button Problem
Junges, Sebastian	Counterexample-Driven Synthesis for Probabilistic Program Sketches
K
Kang, Eunsuk	Alloy*: a general-purpose higher-order relational constraint solver
Kasampalis, Theodoros	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Katoen, Joost-Pieter	Counterexample-Driven Synthesis for Probabilistic Program Sketches
Klein, Joachim	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Krings, Sebastian	Embedding High-Level Formal Specifications into Applications
Krishnamurthi, Shriram	The Human in Formal Methods
Kwiatkowska, Marta	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Körner, Philipp	Embedding High-Level Formal Specifications into Applications
L
Lamers, Arjan	SOA and the Button Problem
Lang, Frédéric	Compositional Verication of Concurrent Systems by Combining Bisimulations
Larsen, Kim G.	L*-Based Learning of Markov Decision Processes
Le, Quang Loc	Concolic Testing Heap-Manipulating Programs
Leavens, Gary T.	Unifying separation logic and region logic to allow interoperability
Leuschel, Michael	Embedding High-Level Formal Specifications into Applications
Liu, Yang	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Lourenço, Cláudio	GOSPEL - Providing OCaml with a Formal Specification Language
Lucanu, Dorel	Unification in Matching Logic
Lunel, Simon	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Luteberget, Bjørnar	Synthesis of Railway Signaling Layout from Local Capacity Specifications
M
Manzanas Lopez, Diego	Star-Based Reachability Analysis of Deep Neural Networks
Maoz, Shahar	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
Marmsoler, Diego	APML: An Architecture Proof Modelling Language
Mateescu, Radu	Compositional Verication of Concurrent Systems by Combining Bisimulations
Mazzanti, Franco	Compositional Verication of Concurrent Systems by Combining Bisimulations
Milicevic, Aleksandar	Alloy*: a general-purpose higher-order relational constraint solver
Milius, Stefan	Generic Partition Refinement and Weighted Tree Automata
Mitsch, Stefan	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic Pegasus: A Framework for Sound Continuous Invariant Generation
Moore, Brandon	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Moscato, Mariano	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Murray, Toby	Value-Dependent Information-Flow Security on Weak Memory Models
Musau, Patrick	Star-Based Reachability Analysis of Deep Neural Networks
Muñoz, César A.	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Müller, David	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
N
Near, Joseph P.	Alloy*: a general-purpose higher-order relational constraint solver
Nguyen, Luan	Star-Based Reachability Analysis of Deep Neural Networks
Norman, Gethin	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Nyberg, Mattias	Conditions of contracts for separating responsibilities in heterogeneous systems
O
Ogawa, Mizuhito	Formal Semantics Extraction from Natural Language Specifications for ARM
P
Pai, Rekha	Static Analysis for Detecting High-Level Races in RTOS Kernels
Pang, Jun	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
Parker, David	Quantitative Verification of Numerical Stability for Kalman Filters Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Paul, Soumya	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
Pereira, Mário	GOSPEL - Providing OCaml with a Formal Specification Language
Phan, Quoc-Sang	Concolic Testing Heap-Manipulating Programs
Pistiner, Or	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
Platzer, André	Pegasus: A Framework for Sound Continuous Invariant Generation An Axiomatic Approach to Liveness for Differential Equations
Poll, Erik	Formal Methods for Security Functionality and for Secure Functionality
R
Roșu, Grigore	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
S
Santos, Gabriel	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Sanán, David	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Schellhorn, Gerhard	Verifying Correctness of Persistent Concurrent Data Structures
Schneider, Gerardo	Gray-Box Monitoring of Hyperproperties
Schröder, Lutz	Generic Partition Refinement and Weighted Tree Automata
Sheinvald, Sarai	Learning Deterministic Variable Automata over Infinite Alphabets
Singh, Abhishek	Static Analysis for Detecting High-Level Races in RTOS Kernels
Smith, Graeme	Value-Dependent Information-Flow Security on Weak Memory Models
Sogokon, Andrew	Pegasus: A Framework for Sound Continuous Invariant Generation
Steffen, Martin	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Steinhöfel, Dominic	Abstract Execution
Strecker, Martin	Reasoning Formally about Database Queries and Updates
Stucki, Sandro	Gray-Box Monitoring of Hyperproperties
Su, Cui	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
Sun, Jun	Concolic Testing Heap-Manipulating Programs
Sánchez, César	Gray-Box Monitoring of Hyperproperties
T
Talpin, Jean-Pierre	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Tan, Yong Kiam	Pegasus: A Framework for Sound Continuous Invariant Generation An Axiomatic Approach to Liveness for Differential Equations
Tappler, Martin	L*-Based Learning of Markov Decision Processes
Titolo, Laura	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Tran, Hoang-Dung	Star-Based Reachability Analysis of Deep Neural Networks
V
van Eekelen, Marko	SOA and the Button Problem
Vu, Anh V.	Formal Semantics Extraction from Natural Language Specifications for ARM
W
Wehrheim, Heike	Verifying Correctness of Persistent Concurrent Data Structures
Westman, Jonas	Conditions of contracts for separating responsibilities in heterogeneous systems
Wißmann, Thorsten	Generic Partition Refinement and Weighted Tree Automata
X
Xiang, Weiming	Star-Based Reachability Analysis of Deep Neural Networks
Y
Yang, Xiao Dong	Star-Based Reachability Analysis of Deep Neural Networks
Z
Zhang, Fuyuan	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Zhang, Yi	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Zhao, Yongwang	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Č
Češka, Milan	Counterexample-Driven Synthesis for Probabilistic Program Sketches
Ș
Șerbănuță, Traian Florin	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Șerbănuță, Virgil	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain

Disclaimer | Powered by EasyChair Smart Program