Verification Center Workshop
| Date: | 2015/06/25 (Thu) 13:00 to 2015/06/26 (Fri) 14:00 |
|---|---|
| Place: | Hotel Arrowle, Kaga |
| Group: | Research Center for Software Verification |
"Verification Center Workshop"
Date: Jun. 25th and 26th, 2015
Place: Hotel Arrowle
Programme
Jun. 25
13:00 Opening
Session 1
13:30 - 14:00 Issues on Algebraic Specification and Verification in CafeOBJ
(by Futatsugi) slides
14:00 - 14:30 Proof scores in OTS/CafeOBJ and proofs with CITP for CafeOBJ
(by Ogata)
14:30 - 15:00 How do we ensure the correctness of products via formal verification?
(by Aoki) slides
15:00 - 15:30 Proving sufficient completeness of constructor-based specifications
(by Nakamura)
15:30 - 16:00 Break
Session 2
16:00 - 16:30 Verifying the Correctness of Tupling Transformations based on Conditional Rewriting
(by Chiba) slides
16:30 - 17:00 TBD
(by Yatsu)
17:00 - 18:30 Discussion
18:30 - 21:30 Dinner Meeting
Jun. 26
Session 3
9:30 - 10:00 CafeOBJ in unusual surroundings
(by Preining) slides
10:00 - 10:30 Break
Session 4
10:30 - 11:00 CafeOBJ: The missing guide
(by Sawada)
11:00 - 11:30 Formalization and Verification of Declarative Cloud Orchestration
(by Yoshida) slides
11:30 - 12:00 Discussion
12:00 - 13:30 Lunch Meeting
13:00 - 14:00 Closing
Abstratcs
Issues on Algebraic Specification and Verification in CafeOBJ
(by Futatsugi)
Abstract: Current issues on developing formal specifications and verifying them in CafeOBJ are tried to be summarized. It is intended to think over the future research possibilities/requirements.
Proof scores in OTS/CafeOBJ and proofs with CITP for CafeOBJ
(by Ogata)
Abstract: The proof that an authentication protocol enjoys the nonce secrecy property is used as an example to describe proof scores written in OTS/CafeOBJ and proofs conducted with CITP for CafeOBJ, a proof assistant for CafeOBJ. The authentication protocol is the Lowe's modification (NSLPK) of the Needham-Schroder Public-Key (NSPK) authentication protocol. The nonce secrecy property (NSP) is that secrets are never leaked to the third party.
How do we ensure the correctness of products via formal verification?
(by Aoki)
Abstract: I realized that there is a big gap between the formal verification of designs and programs, and that of products according to my experience on the verification of automotive operating systems. In this time slot, I would like to have an opportunity to discuss this problem after introducing my awareness.
Proving sufficient completeness of constructor-based specifications
(by Nakamura)
Abstract: CafeOBJ algebraic specification language supports description of specifications whose models are constructor-based algebras. Sufficient completeness is one of the most important properties of constructor-based specifications, which guarantees the existence of initial models. In this study, we give a sufficient condition for sufficient completeness of constructor-based specifications based on the theory of term rewriting.
Verifying the Correctness of Tupling Transformations based on Conditional Rewriting
(by Chiba)
Abstract: Chiba et al.\ (2010) proposed a framework of program transformation by templates based on term rewriting. Their framework can deal with tupling, which improves efficiency of programs. Outputs of their framework, however, may not always be more efficient than inputs. In this paper, we propose a technique to show the correctness of tupling based on conditional term rewriting. We give an extended equational logic in order to add conditional rules.
TBD
(by Yatsu)
Abstract: TBD
CafeOBJ in unusual surroundings
(by Preining)
Abstract: We present recent work on adapting CafeOBJ to fields outside of verification, in particular symbolic computation (polynomials) and exact number representations (signed digit streams). After discussing some problems faced during the development of the code, we give examples and explain the code as well as the mathematical background.
CafeOBJ: The missing guide
(by Sawada)
Abstract: I will present some tips which make your life easier with CafeOBJ interpreter. Many of them are described in current User Manual, but they seem to be not used so much. And there are some new commands for online help which provide you useful informations of the system. All of these should be helpful for users having problem with the usage of CafeOBJ interpreter.
Formalization and Verification of Declarative Cloud Orchestration
(by Yoshida)
Abstract: Automation of cloud system operations is called Cloud Orchestration. A standard specification language, TOSCA (Topology and Orchestration Specification for Cloud Applications), has been proposed to define topologies of cloud applications. I will talk about how to specify behavior of TOSCA topologies as state transition systems and to verify that orchestrated operations always successfully complete by proving the transition systems enjoys leads-to properties.
| Contact | nao-aoki@jaist.ac.jp |
|---|