Compilation of any software program usually involves application of some compiler transformation techniques so that an optimized intermediate code is produced. For validation of all such transformations, one may try to verify the optimizing compiler which is, in general, not even partially decidable. An effective alternative is to establish the computational equivalence between the original and the transformed programs, whereby we can claim that the transformations applied for the specific instance is correct. (Although this problem (of checking equivalence between two programs) too is not semi-decidable, devising a compiler verifier in the spirit of a general program verifier is held to be a much more difficult task). Program equivalence is the problem of proving that two programs are equal under some definition of equivalence, e.g., input-output equivalence. The field captures researchers from formal verification, semantics and logics. Program equivalence is one of the most important problems in formal verification and that is why the topic attracts the interest of several research communities: denotational semantics, deductive software verification, bounded model checking, specification inference, High level synthesis, software evolution and regression testing, etc. On this topic, program equivalence and relational reasoning (PERR) has been conducting since last three years. Not one Dagstuhl seminar was conducted in this topic. The goal of the workshop is to exchange the ideas between researchers who are working on Program Equivalence domain
This workshop aims at gathering researchers and practitioners addressing the challenges induced by program equivalence, in order to identify synergy, common problems, solutions and visions for the future of this area. Strong interactions among participants will be favored to provide constructive feedback for accepted workshop papers and develop future collaborations and community building. A plenary brainstorming and discussion session will be planned at the end of the day. The discussion topics will be selected based on the interests of the participants.
TOPIC OF INTEREST
The workshop welcomes contributions on the topics mentioned below but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyperproperties, in particular of secure information flow.
- Regression verification
- Symbolic execution
- specification of differences between programs
- translation validation
- correct compiler transformations
- code equivalence checking in teaching and marking
- Track 1: Translation Validation
A user written application program goes through significant optimizing and parallelizing transformations, both (compiler) automated and human guided, before being mapped to an architecture. Formal verification of these transformations is crucial to ensure that they preserve the original behavioural specification. In this track, our focus will be to convey several translation validation approaches for various compiler.
- Track 2: Regression verification
Regression verification is the problem of deciding whether two similar programs are equivalent under an arbitrary yet equal context, given some definition of equivalence. In this track our aim is to discuss the challenges of regression verification for both sequential programs and parallel programs. In this track our aim is to demontsrate Reve tool which uses regression verification.
- Track 3: Education Technology
Insufficient investment in education results in low quality of teacher education and inadequate academic infrastructure. Teachers are unable or unwilling to provide support to the learning processes. In this context, digital technologies (aka Information and Communication Technologies, or ICT in short), are sometimes seen as a solution that can address curricular resource shortage, teacher shortage, and teacher quality.
Applying program equivalence concepts in developing auto evaluation system for programing course can significantly improve these implementations and ensure efficiency
Dr. Bandyopadhyay is an Assistant Professor in the Department of Computer Science and Information Systems at the BITS Pilani, K. K. Birla Goa Campus. He received his B.Tech in Computer Science and Engineering from West Bengal University of Technology and Ph.D in computer science and engineering from Indian Institute of Technology, Kharagpur. He was working as HPI-post doctoral fellow at System Analysis and Modeling group, Hasso Plattner Institute, Germany. His current research interests include broadly formal methods in software engineering.
- Full Day workshop
- Soumyadip Bandyopadhyay, BITS Pilani, India