info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
BCS-FACS ProCoS Workshop on Provably Correct Systems, London, UK, 9-10 March 2015
3 views
Skip to first unread message
Jonathan Bowen
Jan 10, 2015, 6:59:38 PM1/10/15
to
BCS-FACS - Formal Aspects of Computing Systems
ProCoS Workshop - Provably Correct Systems
BCS offices, London, UK, 9-10 March 2015
Co-chairs:
Prof. Jonathan Bowen, Birmingham City University, UK
Prof. Mike Hinchey, LERO, University of Limerick, Republic of Ireland
Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
The years 2014 and 2015 mark 25 years and 20 years, respectively, since the start and end of the European ESPRIT ProCoS projects on Provably Correct Systems, inspired by the CLInc project in the US. The ProCoS I/II projects and the associated ProCoS-US initiative ran from 1989-1995, followed by the ProCoS-WG Working Group of 25 partners. The projects aimed to perform research in the fundamental technical aspects of a development process for critical embedded systems, from the original capture of requirements all the way down to the computers and special purpose hardware on which the programs run. The projects were significant in their contributions to provably correct systems, and led directly to a better general understanding of the relationship between a range of theories, and how their combination can be used in the planning and development of critical software tasks. This event marks these 20th and 25th anniversaries of ProCoS to look back at its achievements and to identify key research that will contribute to the next generation of provably correct systems, with invited talks by leading international computer science researchers, many directly involved with the original ProCoS projects.
Online information: http://www.bcs.org/content/ConWebDoc/53939
Online registration: https://events.bcs.org/book/1364
Location information: https://www.bcs.org/upload/pdf/london-office-guide.pdf
£60 for BCS members and student, £120 for non-BCS members
Sponsored by Lero (The Irish Software Engineering Research Centre)
Programme
Monday 9th March 2015 (Whence)
09.00-09.30 Registration
09.30-11.00 Session 1 (Introduction) - Chair: Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
How it all began - Prof. Dines Bjørner, Technical University of Denmark, Denmark
Provably Correct Systems: Whence and whither? - Prof. Jonathan P. Bowen, Birmingham City University, UK
Algebraic proof of consistency of operational and verification semantics - Prof. Tony Hoare, Microsoft Research Cambridge, UK
11.00-11.30 Coffee/tea break
11.30-13.00 Session 2 (Hybrid systems) - Chair: Prof. Jonathan Bowen, Birmingham City University, UK
Hybrid Systems from the ProCoS Gas Burner to Highway Traffic - Prof. Anders P. Ravn, Aalborg University, Denmark
Engineering Arithmetic Constraint Solvers for Automatic Analysis of Hybrid Discrete-continuous Systems - Prof. Dr Martin Fränzle, Carl von Ossietzky Universität Oldenburg , Germany
Hybrid Relation Calculus - Prof. Jifeng He, East China Normal University, China
13.00-14.00 Lunch break
14.00-16.00 Session 3 (Reasoning, Analysis & Refinement) - Chair: Prof. Mike Hinchey, LERO, University of Limerick, Republic of Ireland
Reasoning Abstractly about Concurrency - Prof. Cliff Jones, Newcastle University, UK
Mode-Confusion Analysis using Formal Methods, Deadlock and Livelock Analysis - Prof. Dr Bettina Buth, HAW Hamburg, Germany
Refinement Algebra and Applications - Dr Augusto Sampaio, Universidade Federal de Pernambuco, Brazil
Space for Traffic Manoeuvres - Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
16.00-16.30 Coffee/tea break
16.30-18.45 Session 4 (Mechanization) - Chair: Prof. Dr Debora Weber-Wulff, Hochschule für Technik und Wirtschaft Berlin, Germany
Model Checking Duration Calculus: The DCVALID story - Dr Paritosh Pandya, Tata Institute of Fundamental Research, India
Automatic Verification of Infinite-state Systems - Prof. Dr Markus Müller-Olm, Westfälische Wilhelms-Universität Münster, Germany
Commercial Use of the ACL2 System - Prof. Warren Hunt, University of Austin, Texas, USA
Managing Large Terms Representing Realistic Machine States - Prof. J Strother Moore, The University of Texas at Austin, USA
Real Time Systems 20 Years On - Dr Victoria Coleman, Yahoo
18.45-20.00 Reception
Tuesday 10th March 2015 (Whither)
9.00-10.30 Session 1 (Assertions & Testing) - Chair: Prof. Michael R. Hansen, Technical University of Denmark, Denmark
Run-time Assertion Checking of Data- and Protocol-oriented Properties of Java Programs - Prof. Frank de Boer, CWI, Netherlands
Assertions for Hardware - Prof. Wayne Luk, Imperial College London, UK
Combining Testing and Verification - Prof. Dr Heike Wehrheim, University of Paderborn, Germany
10.30-11.00 Coffee/tea break
11.00-12.30 Session 2 (Proof) - Chair: Dr Hans Rischel, Technical University of Denmark, Denmark
Proof with Event-B/Rodin - Prof. Michael Butler, University of Southampton, UK
Are We There Yet? Twenty year of industrial theorem proving with SPARK - Dr Rod Chapman, Protean Code Ltd, UK
What have we Learned about Proof? - Prof. Ursula Martin, University of Oxford, UK
12.30-13.30 Lunch break
13.30-15.00 Session 3 (Models & ATP) - Chair: Dr Huibiao Zhu
Model-checking Extended Linear Duration Invariants - Prof. Naijun Zhan, Institute of Software, Chinese Academy of Sciences, China
A Model of Cyber-physical Component Systems - Prof. Zhiming Liu, Birmingham City University, UK
Advances in Connection-based Automated Theorem Proving - Prof. Dr Wolfgang Bibel, Darmstadt University of Technology, Germany and Prof. Dr Jens Otten, Potsdam University, Germany
15.00-15.30 Coffee/tea break
15.30-16.30 Session 4 (Correctness) - Chair: Prof. Jim Woodcock, University of York, UK
Synthesis of Provably Correct Systems - Prof. Dr Bernd Finkbeiner, Saarland University, Germany
Linearizability and Correctness for Weak Memory Models - Prof. John Derrick, University of Sheffield, UK
Using Abstract State Machine Nets to Construct Provably Correct Business Processes - Prof. Dr Egon Börger, Università di Pisa, Italy
16.30-16.35 Close
--
Prof. Jonathan Bowen
Professor of Computer Science, Birmingham City University
Emeritus Professor, London South Bank University
Chairman, Museophile Limited
http://www.jpbowen.com
ProCoS Workshop - Provably Correct Systems
BCS offices, London, UK, 9-10 March 2015
Co-chairs:
Prof. Jonathan Bowen, Birmingham City University, UK
Prof. Mike Hinchey, LERO, University of Limerick, Republic of Ireland
Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
The years 2014 and 2015 mark 25 years and 20 years, respectively, since the start and end of the European ESPRIT ProCoS projects on Provably Correct Systems, inspired by the CLInc project in the US. The ProCoS I/II projects and the associated ProCoS-US initiative ran from 1989-1995, followed by the ProCoS-WG Working Group of 25 partners. The projects aimed to perform research in the fundamental technical aspects of a development process for critical embedded systems, from the original capture of requirements all the way down to the computers and special purpose hardware on which the programs run. The projects were significant in their contributions to provably correct systems, and led directly to a better general understanding of the relationship between a range of theories, and how their combination can be used in the planning and development of critical software tasks. This event marks these 20th and 25th anniversaries of ProCoS to look back at its achievements and to identify key research that will contribute to the next generation of provably correct systems, with invited talks by leading international computer science researchers, many directly involved with the original ProCoS projects.
Online information: http://www.bcs.org/content/ConWebDoc/53939
Online registration: https://events.bcs.org/book/1364
Location information: https://www.bcs.org/upload/pdf/london-office-guide.pdf
£60 for BCS members and student, £120 for non-BCS members
Sponsored by Lero (The Irish Software Engineering Research Centre)
Programme
Monday 9th March 2015 (Whence)
09.00-09.30 Registration
09.30-11.00 Session 1 (Introduction) - Chair: Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
How it all began - Prof. Dines Bjørner, Technical University of Denmark, Denmark
Provably Correct Systems: Whence and whither? - Prof. Jonathan P. Bowen, Birmingham City University, UK
Algebraic proof of consistency of operational and verification semantics - Prof. Tony Hoare, Microsoft Research Cambridge, UK
11.00-11.30 Coffee/tea break
11.30-13.00 Session 2 (Hybrid systems) - Chair: Prof. Jonathan Bowen, Birmingham City University, UK
Hybrid Systems from the ProCoS Gas Burner to Highway Traffic - Prof. Anders P. Ravn, Aalborg University, Denmark
Engineering Arithmetic Constraint Solvers for Automatic Analysis of Hybrid Discrete-continuous Systems - Prof. Dr Martin Fränzle, Carl von Ossietzky Universität Oldenburg , Germany
Hybrid Relation Calculus - Prof. Jifeng He, East China Normal University, China
13.00-14.00 Lunch break
14.00-16.00 Session 3 (Reasoning, Analysis & Refinement) - Chair: Prof. Mike Hinchey, LERO, University of Limerick, Republic of Ireland
Reasoning Abstractly about Concurrency - Prof. Cliff Jones, Newcastle University, UK
Mode-Confusion Analysis using Formal Methods, Deadlock and Livelock Analysis - Prof. Dr Bettina Buth, HAW Hamburg, Germany
Refinement Algebra and Applications - Dr Augusto Sampaio, Universidade Federal de Pernambuco, Brazil
Space for Traffic Manoeuvres - Prof. Dr Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg , Germany
16.00-16.30 Coffee/tea break
16.30-18.45 Session 4 (Mechanization) - Chair: Prof. Dr Debora Weber-Wulff, Hochschule für Technik und Wirtschaft Berlin, Germany
Model Checking Duration Calculus: The DCVALID story - Dr Paritosh Pandya, Tata Institute of Fundamental Research, India
Automatic Verification of Infinite-state Systems - Prof. Dr Markus Müller-Olm, Westfälische Wilhelms-Universität Münster, Germany
Commercial Use of the ACL2 System - Prof. Warren Hunt, University of Austin, Texas, USA
Managing Large Terms Representing Realistic Machine States - Prof. J Strother Moore, The University of Texas at Austin, USA
Real Time Systems 20 Years On - Dr Victoria Coleman, Yahoo
18.45-20.00 Reception
Tuesday 10th March 2015 (Whither)
9.00-10.30 Session 1 (Assertions & Testing) - Chair: Prof. Michael R. Hansen, Technical University of Denmark, Denmark
Run-time Assertion Checking of Data- and Protocol-oriented Properties of Java Programs - Prof. Frank de Boer, CWI, Netherlands
Assertions for Hardware - Prof. Wayne Luk, Imperial College London, UK
Combining Testing and Verification - Prof. Dr Heike Wehrheim, University of Paderborn, Germany
10.30-11.00 Coffee/tea break
11.00-12.30 Session 2 (Proof) - Chair: Dr Hans Rischel, Technical University of Denmark, Denmark
Proof with Event-B/Rodin - Prof. Michael Butler, University of Southampton, UK
Are We There Yet? Twenty year of industrial theorem proving with SPARK - Dr Rod Chapman, Protean Code Ltd, UK
What have we Learned about Proof? - Prof. Ursula Martin, University of Oxford, UK
12.30-13.30 Lunch break
13.30-15.00 Session 3 (Models & ATP) - Chair: Dr Huibiao Zhu
Model-checking Extended Linear Duration Invariants - Prof. Naijun Zhan, Institute of Software, Chinese Academy of Sciences, China
A Model of Cyber-physical Component Systems - Prof. Zhiming Liu, Birmingham City University, UK
Advances in Connection-based Automated Theorem Proving - Prof. Dr Wolfgang Bibel, Darmstadt University of Technology, Germany and Prof. Dr Jens Otten, Potsdam University, Germany
15.00-15.30 Coffee/tea break
15.30-16.30 Session 4 (Correctness) - Chair: Prof. Jim Woodcock, University of York, UK
Synthesis of Provably Correct Systems - Prof. Dr Bernd Finkbeiner, Saarland University, Germany
Linearizability and Correctness for Weak Memory Models - Prof. John Derrick, University of Sheffield, UK
Using Abstract State Machine Nets to Construct Provably Correct Business Processes - Prof. Dr Egon Börger, Università di Pisa, Italy
16.30-16.35 Close
--
Prof. Jonathan Bowen
Professor of Computer Science, Birmingham City University
Emeritus Professor, London South Bank University
Chairman, Museophile Limited
http://www.jpbowen.com
0 new messages