Abstract is missing.
- Formal Policy Synthesis for Continuous-State Systems via Reinforcement LearningMilad Kazemi, Sadegh Soudjani. 3-21 [doi]
- Grey-Box Learning of Register AutomataBharat Garhewal, Frits W. Vaandrager, Falk Howar, Timo Schrijvers, Toon Lenaerts, Rob Smits. 22-40 [doi]
- Clustering-Guided SMT($\mathcal {L\!R\!A}$) LearningTim Meywerk, Marcel Walter, Daniel Große, Rolf Drechsler. 41-59 [doi]
- Fast and Effective Well-Definedness CheckingMichael Leuschel. 63-81 [doi]
- An Event-B Based Generic Framework for Hybrid Systems Formal ModellingGuillaume Dupont, Yamine Aït Ameur, Marc Pantel, Neeraj Kumar Singh. 82-102 [doi]
- Towards Generating SPARK from Event-B ModelsSanjeevan Sritharan, Thai Son Hoang. 103-120 [doi]
- Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java ProgramsMalte Mues, Till Schallau, Falk Howar. 123-140 [doi]
- Automatic Generation of Guard-Stable Floating-Point CodeLaura Titolo, Mariano M. Moscato, Marco A. Feliú, César A. Muñoz. 141-159 [doi]
- Formal Methods for GPGPU Programming: Is the Demand Met?Lars B. van den Haak, Anton Wijs, Mark van den Brand, Marieke Huisman. 160-177 [doi]
- Active Objects with Deterministic BehaviourLudovic Henrio, Einar Broch Johnsen, Violet Ka I Pun. 181-198 [doi]
- History-Based Specification and Verification of Java Collections in KeYHans-Dieter A. Hiep, Jinting Bian, Frank S. de Boer, Stijn de Gouw. 199-217 [doi]
- Modular Integration of Crashsafe Caching into a Verified Virtual File System SwitchStefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif. 218-236 [doi]
- Formal Verification of Executable Complementation and Equivalence Checking for Büchi AutomataJulian Brunner 0001. 239-256 [doi]
- A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting AlgorithmsMohsen Safari, Marieke Huisman. 257-275 [doi]
- Synthesizing Clock-Efficient Timed AutomataNeda Saeedloei, Feliks Kluzniak. 276-294 [doi]
- Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock InsertionSander de Putter, Anton Wijs. 297-317 [doi]
- Tight Error Analysis in Fixed-Point ArithmeticStella Simic, Alberto Bemporad, Omar Inverso, Mirco Tribastone. 318-336 [doi]
- Detection of Polluting Test Objectives for Dataflow CriteriaThibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre. 337-345 [doi]
- Meeduse: A Tool to Build and Run Proved DSLsAkram Idani. 349-367 [doi]
- Chain of Events: Modular Process Models for the LawSøren Debois, Hugo A. López, Tijs Slaats, Amine Abbad Andaloussi, Thomas T. Hildebrandt. 368-386 [doi]
- Reformulation of SAT into a Polynomial Box-Constrained Optimization ProblemStéphane Jacquet, Sylvain Hallé. 387-394 [doi]
- PALM: A Technique for Process ALgebraic Specification MiningSara Belluccini, Rocco De Nicola, Barbara Re 0001, Francesco Tiezzi. 397-418 [doi]
- Philosophers May Dine - Definitively!Safouan Taha, Burkhart Wolff, Lina Ye. 419-439 [doi]
- Algebra-Based Loop SynthesisAndreas Humenberger, Nikolaj Bjørner, Laura Kovács. 440-459 [doi]