LOPSTR 

18:00
PPDP and LOPSTR Reception (Welcome Drink and Snacks)
[Location:
Cafe Sturm und Drang (ground floor, Hörsaalzentrum)]

18:00
PPDP and LOPSTR Reception (Welcome Drink and Snacks)
[Location:
Cafe Sturm und Drang (ground floor, Hörsaalzentrum)]

LOPSTR 

08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m.
It is located in the second floor of the building while the conference rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building.

08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m.
It is located in the second floor of the building while the conference rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building.

09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Formal methods for JavaScript (Invited Talk)
Philippa Gardner We present a novel, unified approach to the development of compositional symbolic execution tools, which bridges the gap between traditional symbolic execution and compositional program reasoning based on separation logic. We apply our approach to JavaScript, providing support for full verification, wholeprogram symbolic testing, and automatic compositional testing based on biabduction. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Formal methods for JavaScript (Invited Talk)
Philippa Gardner We present a novel, unified approach to the development of compositional symbolic execution tools, which bridges the gap between traditional symbolic execution and compositional program reasoning based on separation logic. We apply our approach to JavaScript, providing support for full verification, wholeprogram symbolic testing, and automatic compositional testing based on biabduction. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
LOPSTR: Analysis of TRS
[Chair:
Vincent Nys • Location:
HZ 11 (third floor, Hörsaalzentrum)]
10:30
Proving Program Properties as FirstOrder Satisfiability
Salvador Lucas Program semantics can often be expressed as a (manysorted) firstorder theory S, and program properties as sentences φ which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties φ expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of S and the negation ¬φ of φ. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (manysorted) firstorder theo ries. In this paper we extend our previous results to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property φ by just finding a model of an appropri ate theory (including S and possibly something else) and an appropriate firstorder formula related to φ. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects. 11:00
Guided Unfoldings for Finding Loops in Standard Term Rewriting
Étienne Payet In this paper, we reconsider the unfoldingbased technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distin guished positions in the rewrite rules. This results in a depthfirst compu tation of the unfoldings, whereas the original technique was breadthfirst. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs). 11:30
Homeomorphic Embedding modulo Combinations of Associativity and Commutativity Axioms
María Alpuente, Angel CuencaOrtega, Santiago Escobar, and José Meseguer The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and veri fication. However, homeomorphic embedding has never been investigated in the context of ordersorted rewrite theories that support symbolic execution methods modulo equa tional axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homemomorphic embed ding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice. 
10:30
LOPSTR: Analysis of TRS
[Chair:
Vincent Nys • Location:
HZ 11 (third floor, Hörsaalzentrum)]
10:30
Proving Program Properties as FirstOrder Satisfiability
Salvador Lucas Program semantics can often be expressed as a (manysorted) firstorder theory S, and program properties as sentences φ which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties φ expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of S and the negation ¬φ of φ. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (manysorted) firstorder theo ries. In this paper we extend our previous results to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property φ by just finding a model of an appropri ate theory (including S and possibly something else) and an appropriate firstorder formula related to φ. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects. 11:00
Guided Unfoldings for Finding Loops in Standard Term Rewriting
Étienne Payet In this paper, we reconsider the unfoldingbased technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distin guished positions in the rewrite rules. This results in a depthfirst compu tation of the unfoldings, whereas the original technique was breadthfirst. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs). 11:30
Homeomorphic Embedding modulo Combinations of Associativity and Commutativity Axioms
María Alpuente, Angel CuencaOrtega, Santiago Escobar, and José Meseguer The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and veri fication. However, homeomorphic embedding has never been investigated in the context of ordersorted rewrite theories that support symbolic execution methods modulo equa tional axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homemomorphic embed ding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice. 
12:00
Lunch Break
[Location:
Mensa Casino]

12:00
Lunch Break
[Location:
Mensa Casino]

13:30
LOPSTR: Around LogicBased distributed/concurrent programming
[Chair:
Salvador Lucas • Location:
HZ 11 (third floor, Hörsaalzentrum)]
13:30
Multiparty Classical Choreographies
Marco Carbone, Luís CruzFilipe, Fabrizio Montesi, and Agata Murawska We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logicdriven compilation of choreographies with replicated processes. 14:00
Correctbyconstruction Process Composition Using Classical Linear Logic Inference
Petros Papapanagiotou and Jacques Fleuriot The need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear Logic (CLL) for correct byconstruction resourcebased process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting. 14:30
Confluence of CHR revisited: invariants and modulo equivalence
Henning Christiansen and Maja H. Kirkeby Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before. 
13:30
LOPSTR: Around LogicBased distributed/concurrent programming
[Chair:
Salvador Lucas • Location:
HZ 11 (third floor, Hörsaalzentrum)]
13:30
Multiparty Classical Choreographies
Marco Carbone, Luís CruzFilipe, Fabrizio Montesi, and Agata Murawska We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logicdriven compilation of choreographies with replicated processes. 14:00
Correctbyconstruction Process Composition Using Classical Linear Logic Inference
Petros Papapanagiotou and Jacques Fleuriot The need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear Logic (CLL) for correct byconstruction resourcebased process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting. 14:30
Confluence of CHR revisited: invariants and modulo equivalence
Henning Christiansen and Maja H. Kirkeby Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before. 
15:00
Break (No Coffee)
Use this break to walk from the conference location to the start of the city tour (Old Opera Frankfurt).

15:00
Break (No Coffee)
Use this break to walk from the conference location to the start of the city tour (Old Opera Frankfurt).

15:45
Social Event: Guided two hour city walk through the city centre of Frankfurt.
[Location:
The tour starts in front of the Old Opera Frankfurt]
This city walk through the old town centre (Römerberg) focuses on various aspects of Frankfurt's colourful history, including its role as electoral site of German kings and host city for the coronation ceremonies of Holy Roman emperors. Frankfurt's role as a free trade city and site of Germany's first national assembly, held right here at St Paul's Church in 1848, is also highlighted. The tour covers an abundance of significant events within the smallest of geographical areas. 
15:45
Social Event: Guided two hour city walk through the city centre of Frankfurt.
[Location:
The tour starts in front of the Old Opera Frankfurt]
This city walk through the old town centre (Römerberg) focuses on various aspects of Frankfurt's colourful history, including its role as electoral site of German kings and host city for the coronation ceremonies of Holy Roman emperors. Frankfurt's role as a free trade city and site of Germany's first national assembly, held right here at St Paul's Church in 1848, is also highlighted. The tour covers an abundance of significant events within the smallest of geographical areas. 
18:30
Conference Dinner
[Location:
Vinum Frankfurt]

18:30
Conference Dinner
[Location:
Vinum Frankfurt]

LOPSTR 

08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building. 
08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Stuckey • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Constrained Horn Clauses for Verification (Invited Talk)
Jorge Navas Developing scalable software verification tools is a very difficult task. First, due to the undecidability of the verification problem, these tools, must be highly tuned and engineered to provide reasonable efficiency and precision tradeoffs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. This talk presents SeaHorn — an open source automated Constrained Horn clausebased reasoning framework. SeaHorn combines advanced automated solving techniques based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is built on top of LLVM using its frontend(s) to deal with the idiosyncrasies of the syntax and it highly benefits from LLVM optimizations to reduce the verification effort. SeaHorn uses Constrained Horn clauses (CHC) which are a uniform way to formally represent a broad variety of transition systems while allowing many encoding styles of verification conditions. Moreover, the recent popularity of CHC as an intermediate language for verification engines makes it possible to interface SeaHorn with a variety of new and emerging tools. All of these features make SeaHorn a versatile and highly customizable tool which allows researchers to easily build or experiment with new verification techniques. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Stuckey • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Constrained Horn Clauses for Verification (Invited Talk)
Jorge Navas Developing scalable software verification tools is a very difficult task. First, due to the undecidability of the verification problem, these tools, must be highly tuned and engineered to provide reasonable efficiency and precision tradeoffs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. This talk presents SeaHorn — an open source automated Constrained Horn clausebased reasoning framework. SeaHorn combines advanced automated solving techniques based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is built on top of LLVM using its frontend(s) to deal with the idiosyncrasies of the syntax and it highly benefits from LLVM optimizations to reduce the verification effort. SeaHorn uses Constrained Horn clauses (CHC) which are a uniform way to formally represent a broad variety of transition systems while allowing many encoding styles of verification conditions. Moreover, the recent popularity of CHC as an intermediate language for verification engines makes it possible to interface SeaHorn with a variety of new and emerging tools. All of these features make SeaHorn a versatile and highly customizable tool which allows researchers to easily build or experiment with new verification techniques. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
LOPSTR: Analysis of LP
[Chair:
Michael Hanus • Location:
HZ 11 (third floor, Hörsaalzentrum)]
10:30
Compiling Control as Offline Conjunctive Partial Deduction
Vincent Nys and Danny De Schreye We present a new approach to a technique known as compiling control, whose aim is to compile away special mechanisms for nonstandard atom selection in logic programs. It has previously been conjectured that compiling control could be implemented as an instance of the first Futamura projection, in which an interpreter is specialized for an input program. However, the exact nature of such an interpreter and of the required technique for specialization were never specified. In this work, we propose a Prolog metainterpreter which applies the desired nonstandard selection rule and which is amenable to specialization using offline partial deduction. After the initial analysis phase of compiling control, we collect annotations to specialize the interpreter using the Logen system for offline partial deduction. We also show that the result of the specialization is equivalent to the program obtained using the traditional approach to compiling control. In this way, we simplify the synthesis step. 11:00
Predicate Specialization for Definitional Higherorder Logic Programs
Antonis Troumpoukis and Angelos Charalambidis Higherorder logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higherorder characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higherorder logic programs and can transform them into firstorder programs without introducing additional data structures. The resulting firstorder programs can be executed by conventional logic programming interpreters and benefit from other optimizations that might offer. We provide an implementation and experimental results that suggest the efficiency of the transformation. 11:30
An Assertion language for slicing Constraint Logic Languages
Moreno Falaschi and Carlos Olarte Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we have developed a framework for dynamic slicing of CCP where the user first identifies that a (partial) computation is wrong. Then, she marks (selects) some parts of the final state corresponding to the data (constraints) and processes that she wants to study more deeply. An automatic process of slicing begins, and the partial computation is depurated by removing irrelevant information. In this paper we give two major contributions. First, we extend the framework to CLP, thus generalizing the previous work. Second, we provide an assertion language suitable for both, CCP and CLP, which allows the user to specify some properties of the computations in her program. If a state in a computation does not satisfy an assertion then some wrong information is identified and an automatic slicing process can start. This way we make one step further towards automatizing the slicing process. We show that our framework can be integrated with the previous semiautomatic one, giving the user more choices and flexi bility. We show by means of examples and experiments the usefulness of our approach. 
10:30
LOPSTR: Analysis of LP
[Chair:
Michael Hanus • Location:
HZ 11 (third floor, Hörsaalzentrum)]
10:30
Compiling Control as Offline Conjunctive Partial Deduction
Vincent Nys and Danny De Schreye We present a new approach to a technique known as compiling control, whose aim is to compile away special mechanisms for nonstandard atom selection in logic programs. It has previously been conjectured that compiling control could be implemented as an instance of the first Futamura projection, in which an interpreter is specialized for an input program. However, the exact nature of such an interpreter and of the required technique for specialization were never specified. In this work, we propose a Prolog metainterpreter which applies the desired nonstandard selection rule and which is amenable to specialization using offline partial deduction. After the initial analysis phase of compiling control, we collect annotations to specialize the interpreter using the Logen system for offline partial deduction. We also show that the result of the specialization is equivalent to the program obtained using the traditional approach to compiling control. In this way, we simplify the synthesis step. 11:00
Predicate Specialization for Definitional Higherorder Logic Programs
Antonis Troumpoukis and Angelos Charalambidis Higherorder logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higherorder characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higherorder logic programs and can transform them into firstorder programs without introducing additional data structures. The resulting firstorder programs can be executed by conventional logic programming interpreters and benefit from other optimizations that might offer. We provide an implementation and experimental results that suggest the efficiency of the transformation. 11:30
An Assertion language for slicing Constraint Logic Languages
Moreno Falaschi and Carlos Olarte Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we have developed a framework for dynamic slicing of CCP where the user first identifies that a (partial) computation is wrong. Then, she marks (selects) some parts of the final state corresponding to the data (constraints) and processes that she wants to study more deeply. An automatic process of slicing begins, and the partial computation is depurated by removing irrelevant information. In this paper we give two major contributions. First, we extend the framework to CLP, thus generalizing the previous work. Second, we provide an assertion language suitable for both, CCP and CLP, which allows the user to specify some properties of the computations in her program. If a state in a computation does not satisfy an assertion then some wrong information is identified and an automatic slicing process can start. This way we make one step further towards automatizing the slicing process. We show that our framework can be integrated with the previous semiautomatic one, giving the user more choices and flexi bility. We show by means of examples and experiments the usefulness of our approach. 
12:00
Lunch Break
[Location:
Mensa Casino]

12:00
Lunch Break
[Location:
Mensa Casino]

13:30
LOPSTR: Invited Tutorial #1
[Chair:
Moreno Falaschi • Location:
HZ 11 (third floor, Hörsaalzentrum)]
The VeriMAP System for program transformation and verification (Invited Tutorial)
Fabio Fioravanti Constrained Horn Clauses (CHC) are becoming very popular for representing programs and verification problems, and several tools have been developed for checking their satisfiability.

13:30
LOPSTR: Invited Tutorial #1
[Chair:
Moreno Falaschi • Location:
HZ 11 (third floor, Hörsaalzentrum)]
The VeriMAP System for program transformation and verification (Invited Tutorial)
Fabio Fioravanti Constrained Horn Clauses (CHC) are becoming very popular for representing programs and verification problems, and several tools have been developed for checking their satisfiability.

15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:30
LOPSTR: Program Analysis
[Chair:
Maja Kirkeby • Location:
HZ 11 (third floor, Hörsaalzentrum)]
15:30
Multivariant Assertionbased Guidance in Abstract Interpretation
Isabel GarciaContreras, Jose F. Morales, and Manuel V. Hermenegildo Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision and/or shorten analysis time. This allows dealing with, e.g., constructs for which the analysis is not complete and loses precision or for which the source is only partially available. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance / contextsensitivity, and can handle different runtime semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating convergence, and provide a procedure to decide whether the invariants used to guide the analyzer are checked, incompatible, or neither. We also provide some formal results on the effects of such assertions on the analysis results. 16:00
Eliminating Unstable Tests in FloatingPoint Programs
Laura Titolo, César Muñoz, Marco A. Feliú, and Mariano M. Moscato Roundoff errors arising from the difference between real numbers and their floatingpoint representation cause the control flow of conditional floatingpoint statements to deviate from the ideal flow of the realnumber computation. This problem, which is called test instability, may result in a significant difference between the computation of a floatingpoint program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floatingpoint program that is guaranteed to return either the result of the original floatingpoint program when it can be assured that both its real and its floatingpoint flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems. 16:30
Formalisation of a frame stack semantics for a Javalike language
Aleksy Schubert and Jacek Chrząszcz We present a Coq formalisation of the smallstep operational semantics of Jafun, a small Javalike language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a complex value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the un typed version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it. 
15:30
LOPSTR: Program Analysis
[Chair:
Maja Kirkeby • Location:
HZ 11 (third floor, Hörsaalzentrum)]
15:30
Multivariant Assertionbased Guidance in Abstract Interpretation
Isabel GarciaContreras, Jose F. Morales, and Manuel V. Hermenegildo Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision and/or shorten analysis time. This allows dealing with, e.g., constructs for which the analysis is not complete and loses precision or for which the source is only partially available. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance / contextsensitivity, and can handle different runtime semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating convergence, and provide a procedure to decide whether the invariants used to guide the analyzer are checked, incompatible, or neither. We also provide some formal results on the effects of such assertions on the analysis results. 16:00
Eliminating Unstable Tests in FloatingPoint Programs
Laura Titolo, César Muñoz, Marco A. Feliú, and Mariano M. Moscato Roundoff errors arising from the difference between real numbers and their floatingpoint representation cause the control flow of conditional floatingpoint statements to deviate from the ideal flow of the realnumber computation. This problem, which is called test instability, may result in a significant difference between the computation of a floatingpoint program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floatingpoint program that is guaranteed to return either the result of the original floatingpoint program when it can be assured that both its real and its floatingpoint flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems. 16:30
Formalisation of a frame stack semantics for a Javalike language
Aleksy Schubert and Jacek Chrząszcz We present a Coq formalisation of the smallstep operational semantics of Jafun, a small Javalike language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a complex value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the un typed version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it. 
LOPSTR 

08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference room of LOPSTR (lecture hall HZ 10) is located in the third floor of the building and the room SH1.101 is in another building (Seminarhaus). 
08:30
Registration
[Location:
2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference room of LOPSTR (lecture hall HZ 10) is located in the third floor of the building and the room SH1.101 is in another building (Seminarhaus). 
09:00
LOPSTR & WFLP: Joint Invited Talk
[Chair:
Pedro Lopez • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Experiences in designing scalable static analyses (Invited Talk)
Laure Gonnord Proving the absence of bugs in a given software (problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers). In this talk I will present some experiences in the design of scalable static analyses inside compilers, and try to make a synthesis about the general framework we, together with my coauthors, used to develop them. I will also show some experimental evidence of the impact of this work on realworld compilers, as well as future perspective for this area of research. Keywords: Static Analysis, Abstract Interpretation, Compilation, Code Optimisation. 
09:00
LOPSTR & WFLP: Joint Invited Talk
[Chair:
Pedro Lopez • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Experiences in designing scalable static analyses (Invited Talk)
Laure Gonnord Proving the absence of bugs in a given software (problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers). In this talk I will present some experiences in the design of scalable static analyses inside compilers, and try to make a synthesis about the general framework we, together with my coauthors, used to develop them. I will also show some experimental evidence of the impact of this work on realworld compilers, as well as future perspective for this area of research. Keywords: Static Analysis, Abstract Interpretation, Compilation, Code Optimisation. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
LOPSTR: Invited Tutorial #2
[Chair:
Fred Mesnard • Location:
HZ 10 (third floor, Hörsaalzentrum)]
25 years of Ciao (Invited Tutorial)
Manuel Hermenegildo Ciao is a logicbased, multiparadigm programming language which has pioneered over the years many interesting language and programming environmentrelated concepts. An example is the notion of programming languages as modular languagebuilding tools rather than closed designs. Another is the idea of dynamic languages that can optionally and gradually offer formal guarantees, which is also a solution for the classic dichotomy between dynamic and static typing: Ciao has many dynamic features (e.g., dynamically typed, dynamic program modification) but includes an assertion language for (optionally) declaring program properties and powerful tools for static inference and static/dynamic checking of such assertions, testing, documentation, etc. We will provide a handson overview of these features, concentrating on the novel aspects, the motivations behind their design and implementation, their evolution over time, and, specially, their use. In particular, we will show how the system can be used not only as a programming tool and as a language design tool, but also as a generalpurpose program analysis and verification tool, based on the technique of translating program semantics (ranging from source to bytecode, LLVM, or assembly) into Hornclause representation, and idea which Ciao also introduced early on. Finally, we will present some recent work in areas such as scalability, incrementality, or static vs. dynamic costs, as well as some future plans and ideas. 
10:30
LOPSTR: Invited Tutorial #2
[Chair:
Fred Mesnard • Location:
HZ 10 (third floor, Hörsaalzentrum)]
25 years of Ciao (Invited Tutorial)
Manuel Hermenegildo Ciao is a logicbased, multiparadigm programming language which has pioneered over the years many interesting language and programming environmentrelated concepts. An example is the notion of programming languages as modular languagebuilding tools rather than closed designs. Another is the idea of dynamic languages that can optionally and gradually offer formal guarantees, which is also a solution for the classic dichotomy between dynamic and static typing: Ciao has many dynamic features (e.g., dynamically typed, dynamic program modification) but includes an assertion language for (optionally) declaring program properties and powerful tools for static inference and static/dynamic checking of such assertions, testing, documentation, etc. We will provide a handson overview of these features, concentrating on the novel aspects, the motivations behind their design and implementation, their evolution over time, and, specially, their use. In particular, we will show how the system can be used not only as a programming tool and as a language design tool, but also as a generalpurpose program analysis and verification tool, based on the technique of translating program semantics (ranging from source to bytecode, LLVM, or assembly) into Hornclause representation, and idea which Ciao also introduced early on. Finally, we will present some recent work in areas such as scalability, incrementality, or static vs. dynamic costs, as well as some future plans and ideas. 
12:00
Lunch Break
[Location:
Mensa Casino]

12:00
Lunch Break
[Location:
Mensa Casino]
