We are glad to report here the names of the speakers and contents of the joint invited speaker of PPDP 2023 and LOPSTR 2023, to be held as part of SPLASH 2023 in October at Cascais, Lisbon, Portugal.
Maribel Fernández (King’s College London, UK)
- Date: Monday October 23rd, 11 AM
- Title: Unification modulo equational theories in languages with binding operators
- Abstract: Unification (i.e., solving equations between terms) is a key step in the implementation of logic programming languages and theorem provers, and is also used in type inference algorithms for functional languages and as a mechanism to analyse rewrite-based specifications (e.g., to find critical pairs). Matching is a version of unification in which only one of the terms in the equation can be instantiated. Often, operators satisfy equational axioms (e.g., associativity, commutativity), which must be taken into account during the unification or matching process. In addition, when the expressions to be unified involve binding operators (as is the case when representing programs, logics, computation models, etc.), unification and matching algorithms must take into account the alpha-equivalence relation generated by the binders. In this talk, we present matching and unification algorithms for languages that include binding operators as well as operators that satisfy equational axioms, such as associativity and commutativity.
Manuel Hermenegildo (IMDEA Software Institute and Universidad Politecnica de Madrid, Spain)
- Date: Tuesday, October 24th, 9 AM
- Title: On-The-Fly Verification via Incremental, Interactive Abstract Interpretation with CiaoPP and VeriFly
- Abstract: Ciao Prolog pioneered the idea of being able to optionally and gradually add assertions or contracts to programs in order to offer formal guarantees, a now very popular solution for solving the classic trade-offs between dynamic and static languages. This approach is enabled by Ciao’s program analysis and verification framework, CiaoPP, which performs abstract interpretation-based, context- and path-sensitive analysis to infer information against which assertions are checked to achieve verification or flag errors statically. The framework supports multiple other languages in addition to Prolog, from machine code to smart contracts, by translation into Horn clauses. Program semantics is computed over different user-definable abstract domains, via efficient fixpoint computation. This allows inference and verification of both functional and non-functional properties, including, e.g., energy or ’gas’ consumption.
While this type of verification can be performed offline (e.g., as part of continuous integration) it is very useful when it occurs interactively during software development, flagging errors as the program is written. However, while context- and path-sensitive global analysis over complex domains can provide the precision needed for effective verification and optimization, it can also be expensive when applied to large code bases, sometimes making interactive use impractical. On the other hand, in many program development situations modifications are small and isolated within a few components. The modular and incremental fixpoint algorithms used by CiaoPP take advantage of this to reuse as much as possible previous analysis results, reducing response times in interactive use.
In this talk we will review these ideas and show how the integration of the Ciao abstract interpretation framework within different IDEs takes advantage of our efficient and incremental fixpoint to achieve effective verification on-the-fly, as the program is developed. We also demonstrate a number of embeddings of this framework within the browser, and show as an example an application for building interactive tutorials, which we have used for teaching verification and abstract interpretation.
These invited speakers are sponsored by ALP.