Journal: Formal Asp. Comput.

Volume 30, Issue 6

627 -- 628Bernhard K. Aichernig, Carlo A. Furia, Marie-Claude Gaudel, Robert M. Hierons. Special section of Tests and Proofs 2016
629 -- 657Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand. How testing helps to diagnose proof failures
659 -- 684Catherine Dubois, Alain Giorgetti. Tests and proofs for custom data generators
685 -- 711Roberto Bruni, Roberto Giacobazzi, Roberta Gori. Code obfuscation against abstraction refinement attacks
713 -- 738Wanling Xie, Shuangqing Xiang, Huibiao Zhu. A UTP approach for rTiMo
739 -- 757Zhiping Shi, Aixuan Wu, Xiumei Yang, Yong Guan, Yongdong Li, Xiaoyu Song. Formal analysis of the kinematic Jacobian in screw theory
759 -- 0Rosemary Monahan. Daniel Kroening and Ofer Strichman: Decision procedures - Springer Verlag, 2016, XXI, +356 ISBN 978-3-662-50496-3 (Hardback, €69, 67), http: //
761 -- 762Jonathan P. Bowen. Egon Börger and Alexander Raschke: Modeling companion for software practitioners - Springer, 2018, XXI+349 pp, ISBN: 978-3-662-56639-8 (Paperback, £ 46.99), eISBN: 978-3-662-56641-1 (eBook, £ 36.99), http: //

Volume 30, Issue 5

493 -- 494Nikolaj Bjørner, Frank S. de Boer, Andrew Butterfield. Editorial
495 -- 523Nadia Polikarpova, Julian Tschannen, Carlo A. Furia. A fully verified container library
525 -- 544Hamid Bagheri, Eunsuk Kang, Sam Malek, Daniel Jackson 0001. A formal approach for detection of security flaws in the android permission system
545 -- 569David Schneider 0001, Michael Leuschel, Tobias Witt. Model-based problem solving for university timetable validation and improvement
571 -- 595Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham. Automated circular assume-guarantee reasoning
597 -- 625John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim. Mechanized proofs of opacity: a comparison of two techniques

Volume 30, Issue 3-4

333 -- 349Filipe Santos, Krystian Kwiecinski, Ana de Almeida, Sara Eloy, Bruno Taborda. Alternative shaper: a model for automatic design generation
351 -- 380Ling Shi, Yongxin Zhao, Yang Liu 0003, Jun Sun 0001, Jin Song Dong, Shengchao Qin. A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
381 -- 441Yuyan Bao, Gary T. Leavens, Gidon Ernst. Unifying separation logic and region logic to allow interoperability
443 -- 462Yaping Jing, Andrew S. Miner. Computation tree measurement language (CTML)
463 -- 489Raphaël Chane-Yack-Fa, Marc Frappier, Amel Mammar, Alain Finkel. Parameterized verification of monotone information systems
491 -- 492Stefan Hallerstede. Tobias Nipkow and Gerwin Klein: Concrete Semantics with Isabelle/HOL - Springer Verlag, 2014, x + 289 pp, € 63, 29 (Hardback), ISBN 978-3-319-10542-0, http: //

Volume 30, Issue 2

193 -- 217Jianwen Li, Lijun Zhang 0001, Shufang Zhu, Geguang Pu, Moshe Y. Vardi, Jifeng He. An explicit transition system construction approach to LTL satisfiability checking
219 -- 237Hui Zhang, Jinzhao Wu. Formal verification and quantitative metrics of MPSoC data dynamics
239 -- 277Jan Bækgaard Pedersen, Peter H. Welch. The symbiosis of concurrency and verification: teaching and case studies
279 -- 317Riccardo Sisto, Piergiuseppe Bettassa Copet, Matteo Avalle, Alfredo Pironti 0001. Formally sound implementations of security protocols with JavaSPI
319 -- 332Khaled El-Fakih, Nina Yevtushenko, Natalia Kushik. Adaptive distinguishing test cases of nondeterministic finite state machines: test case derivation and length estimation

Volume 30, Issue 1

1 -- 0Ewen Denney, Perdita Stevens, Andrzej Wasowski. Editorial
3 -- 43Sander de Putter, Anton Wijs. A formal verification technique for behavioural model-to-model transformations
45 -- 75Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier. ProFeat: feature-oriented engineering for family-based probabilistic model checking
77 -- 106Marcus Gerhold, Mariëlle Stoelinga. Model-based testing of probabilistic systems
107 -- 131Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall. Cut branches before looking for bugs: certifiably sound verification on relaxed slices
133 -- 162Daniel Strüber 0001, Julia Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer, Jennifer Plöger. Variability-based model transformation: formal foundation and application
163 -- 192Claudio Corrodi, Alexander Heußner, Christopher M. Poskitt. A semantics comparison workbench for a concurrent, asynchronous, distributed programming language