The 13th International Workshop on Automated Verification of Critical Systems took place at the University of Surrey in Guildford, Surrey from 11-13th September, 2013.
AVOCS 2014 University of Twente, The Netherlands
Introduction by Jaco van de Pol to AVOCS 2014.AVOCS 2013 Science of Computer Programming Call For Papers
Special Issue Call for Papers AVOCS 2014, deadline 7 June, 2014.AVOCS 2013 Technical Report
Download technical report here.AVOCS 2013 Group Photo
Take a look here!. Markus also took many pictures during the workshop and they can be seen on Markus' AVOCS pictures weblink.
Invited Speakers
We are grateful to the invited speakers who provided excellent talks during the conference- Sofia Guerra, Partner, Adelard, UK. The title of her talk was:
Keeping the temperature down: assessing smart instruments for the nuclear industry.
Sofia Guerra is a partner at Adelard. She has been project manager of numerous projects funded by the UK, French, US, Finnish and Swedish nuclear industry, regarding the safety assessment, justification and reliability estimation of software-based systems and, in particular, the assessment of smart instruments software. She was part of the Independent Safety Advisor/Auditor team for several UK defence projects including Bowman. She is registered as a software expert with MHRA and regularly assesses the software component of medical devices. She has a PhD in Mathematics (1999) from Lisbon Institute of Technology, Portugal.
- Alessio Lomuscio is Professor in logic for multi-agent systems in the Department of Computing, Imperial College London.
His talk was on Verification of multi-agent systems via model-checking.
Alessio leads the VAS (verification of autonomous systems) research group. He currently holds an EPSRC Leadership Fellowship. He received a PhD in Computer Science from the University of Birmingham in 1999 and a Laurea in Electronic Engineering from Politecnico di Milano in 1995. Before joining Imperial he was Lecturer at King's College London and Senior Lecturer at University College London. His research interests concern the specification and verification of multi-agent systems by means of techniques based on computational logic. In particular he has made theoretical contributions in the area of logic for multi-agent systems (including studying the completeness, decidability and complexity of several temporal-epistemic formalisms) and has put forward several symbolic model checking techniques for the verification of agent-based systems. He has applied these techniques to the verification of a range of applications including autonomous underwater vehicles, web-services and security protocols including e-voting. He is co-author of MCMAS, an open-source, BDD-based model checker for multi-agent systems developed at the VAS research group at Imperial.
- Marco Roveri, Senior Researcher Fondazione Bruno Kessler, Italy. His talk will be on Software Model Checking With Explicit Scheduler and Symbolic Threads. The talk referred to the software model checker Kratos and its use in the railway domain.
Marco is a senior researcher in the Embedded Systems Unit of the Fondazione Bruno Kessler, Trento, Italy. He received a Ph.D. degree in Computer Science from the University of Milano, Italy in 2002. He joined the Automated Reasoning Division of the Istituto Trentino di Cultura, Trento, Italy, in 1998, first as a consultant, and in 2002 as a full time researcher. In 2008 he was appointed as a senior researcher in the Embedded Systems Unit of the Fondazione Bruno Kessler, Trento, Italy. His research interests include automated formal verification of hardware and software systems, formal requirements validation of embedded systems, and automated model based planning.
About AVoCS
The aim of AVoCS 2013 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, security-critical, business-critical, performance-critical, etc). Contributions that describe different techniques, or industrial case studies are encouraged. The technical programme will consist of invited and contributed talks and also allow for short presentations of ongoing work. The workshop will be relatively informal, with an emphasis on discussion.
Sponsorship
We are grateful to Formal Methods Europe and IBM for their generous sponsorship of this event.
