Journal: Formal Asp. Comput.

Volume 33, Issue 6

827 -- 0Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa, Heike Wehrheim. Editorial
829 -- 854Bjørnar Luteberget, Christian Johansen. Drawing with SAT: four methods and A tool for producing railway infrastructure schematics
855 -- 884Simon Foster 0001, Yakoub Nemouchi, Mario Gleirscher, Ran Wei, Tim Kelly. Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
885 -- 921Clemens Dubslaff, Patrick Koopmann, Anni-Yasmin Turhan. Enhancing Probabilistic Model Checking with Ontologies
923 -- 924Alessandro Fantechi, Anne E. Haxthausen, Jim Woodcock. Editorial
925 -- 955Jan Peleska 0001, Niklas Krafczyk, Anne E. Haxthausen, Ralf Pinger. Efficient data validation for geographical interlocking systems
957 -- 987Davide Basile 0001, Alessandro Fantechi, Luigi Rucher, Gianluca Mandò. Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker
989 -- 1007Francesco Flammini, Stefano Marrone 0001, Roberto Nardone, Valeria Vittorini. Compositional modeling of railway Virtual Coupling with Stochastic Activity Networks
1009 -- 1036Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Yamine Aït Ameur, Fuyuki Ishikawa, Alexander B. Romanovsky. A refinement-based development of a distributed signalling system
1037 -- 0Jordi Cabot, Heike Wehrheim, Eerke A. Boiten. Editorial
1039 -- 1066Claudio Menghi, Alessandro Maria Rizzi, Anna Bernasconi 0002, Paola Spoletini. TOrPEDO: witnessing model correctness with topological proofs
1067 -- 1114Patrick Stünkel, Harald König, Yngve Lamo, Adrian Rutle. Comprehensive Systems: A formal foundation for Multi-Model Consistency Management
1115 -- 1145Nils Weidmann, Anthony Anjorin. Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming
1147 -- 1172Maxime Cordy, Sami Lazreg, Mike Papadakis, Axel Legay. Statistical model checking for variability-intensive systems: applications to bug detection and minimization
1173 -- 1208Juan de Lara, Esther Guerra. Language Family Engineering with Product Lines of Multi-level Models
1209 -- 1248Rolf Hennicker, Alexander Knapp, Alexandre Madeira. Hybrid dynamic logic institutions for event/data-based systems
1249 -- 1277Blair Archibald, Géza Kulcsár, Michele Sevegnani. A tale of two graph models: a case study in wireless sensor networks
1279 -- 1280Reinhard Wilhelm. Foundations of programming languages

Volume 33, Issue 4

459 -- 460Annabelle McIver, Maurice H. ter Beek. Editorial
461 -- 518Yong Kiam Tan, André Platzer. An axiomatic approach to existence and liveness for differential equations
519 -- 545Hoang-Dung Tran, Neelanjana Pal, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson. Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
547 -- 573John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim. Verifying correctness of persistent concurrent data structures: a sound and complete method
575 -- 615Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci 0001, Maria Eichlseder, Kim G. Larsen. *-based learning of Markov decision processes (extended version)
617 -- 636Frank S. de Boer, Marcello M. Bonsangue. Symbolic execution formally explained
637 -- 667Milan Ceska 0002, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems
669 -- 693Alexandros Evangelidis, David Parker 0001. Quantitative verification of Kalman filters
695 -- 727Thorsten Wißmann, Hans-Peter Deifel, Stefan Milius, Lutz Schröder. From generic partition refinement to weighted tree automata minimization
729 -- 761Gal Amram, Shahar Maoz, Or Pistiner. GR(1)*: GR(1) specifications extended with existential guarantees
763 -- 802Mario Gleirscher, Radu Calinescu, Jim Woodcock. RiskStructures: A design algebra for risk-aware machines
803 -- 826Gerard Ekembe Ngondi. Denotational semantics of channel mobility in UTP-CSP

Volume 33, Issue 3

299 -- 300Xiaoping Chen, Zhiming Liu, Ji Wang, Jim Woodcock. Editorial
301 -- 323Lei Bu, Yongjuan Liang, Zhunyi Xie, Hong Qian, Yi-Qi Hu, Yang Yu 0001, Xin Chen 0027, Xuandong Li. Machine learning steered symbolic execution framework for complex software code
325 -- 341Huihui Wu, Deyun Lv, Tengxiang Cui, Gang Hou, Masahiko Watanabe, Weiqiang Kong. SDLV: Verification of Steering Angle Safety for Self-Driving Cars
343 -- 384Zhibin Yang, Yang Bao, Yongqiang Yang, Zhiqiu Huang, Jean-Paul Bodeveix, Mamoun Filali, Zonghua Gu. Exploiting augmented intelligence in the modeling of safety-critical autonomous systems
385 -- 406Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Inferring Switched Nonlinear Dynamical Systems
407 -- 435Pengfei Yang, Jianlin Li, Jiangchao Liu, Cheng-Chao Huang, Renjue Li, Liqian Chen, Xiaowei Huang 0001, Lijun Zhang 0001. Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation
437 -- 455Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu 0001, Jim Woodcock. Learning safe neural network controllers with barrier certificates
457 -- 458Michele Loreti. Semantics of the probabilistic Lambda Calculus By Dirk Draheim

Volume 33, Issue 2

151 -- 183Wenbo Zhang 0004, Xian Xu 0001, Qiang Yin, Huan Long. On the Interactive Power of Higher-order Processes Extended with Parameterization
185 -- 205Wim H. Hesselink. UNITY and Büchi automata
207 -- 249Wanling Xie, Huibiao Zhu, Qiwen Xu. A process calculus BigrTiMo of mobile systems and its formal semantics
251 -- 295Marco Bozzano, Alessandro Cimatti, Marco Gario, David Jones, Cristian Mattarei. Model-based Safety Assessment of a Triple Modular Generator with xSAP
297 -- 298Matteo Rossi. Modeling and analysis of communicating systems

Volume 33, Issue 1

1 -- 2Erik P. de Vink, Ana Cavalcanti. Editorial
3 -- 25Giovanni Bacci 0001, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, Pierre-Alain Reynier. Optimal and robust controller synthesis using energy timed automata with uncertainty
27 -- 63Davide G. Cavezza, Dalal Alrajeh, András György 0001. A Weakness Measure for GR(1) Formulae
65 -- 86Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, François Bobot. Formal analysis of the compact position reporting algorithm
87 -- 125Signe Geisler, Anne Elisabeth Haxthausen. Stepwise development and model checking of a distributed interlocking system using RAISE
127 -- 150Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet. Modular verification of programs with effects and effects handlers