Date: November 19, 2019
Place: Alice and Bob (B11-B13)
Chairs: Emmanuel Jeandel
9h15-9h30 Welcome
Session 1 : 9h30-10h30
Pierre Lermusiaux
Pattern Eliminating Transformation #T1
Program transformation is a common practice in computer science, and its many applications can have a range of different objectives. For example, a program written in an original high level language could be either translated into machine code for execution purposes, or towards a language suitable for formal verification. Languages often have a lot of different constructions, and thus, transformations often focus on eliminating some of these constructions, or at least processing some specific sequence of constructions. Rewriting is a widely established formalism to describe the mechanism and the logic behind such transformations. It relies mainly on the principle of rewrite rules to describe the different operations performed. Generally type-preserving, these rewrite rules can ensure that the transformation result has a given type and thus give syntactic guarantees on the constructions it consists of. However, we sometimes want the transformation to provide more guarantees on the shape of its result by specifying that some patterns of constructions does not appear. For this purpose, we propose an approach based on annotatingtransformation function symbols with (anti-)pattern in order for such transformation to guarantee stronger properties on the shape of its result. ith the generic principles governing termalgebra and rewriting, we believe this approach to be an accurate formalism to any language providing pattern-matching primitives.
Hans-Jorg Schurr
Experiments on Improving Quantifier Instantiation #T2
veriT is a state of the art Satisfiability Modulo Theories (SMT) solver. Given an unsatisfiable input problem, veriT can output a certificate – a proof – of its unsatisifiability. These proofs serveat least two purposes. On the one hand, they can be checked by an external proof checker, relieving the SMT solver from the responsibility of being trustworthy, on the other hand they can beused by client systems for further processing. In the past the proofs generated by veriT have been partially reconstructed in the interactive theorem prover Isabelle/HOL. We discuss ongoing workonimproving SMT proof production. While work is constrained by the architecture of the SMT solver, the requirements on the format are given by typical use cases. Overall, our goal is to ensureveriT produces proofs which are easy to check, while maintaining performance.
10h30-11h00 : Coffee
Session 2 : 11h00-12h30
Daniel El Ouraoui
Extending SMT Solvers to Higher-Order Logic #T3
SMT solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic (FOL). Nevertheless, higher-order logic (HOL) within SMTis still little explored. I’ll present an extension for SMT solvers to natively support HOL reasoning without compromising performance on FOL reasoning, thus leveraging the extensive research and implementation efforts dedicated to efficient SMT solving. I’ll show how to generalize data structures and the ground decision procedure to support partial applications and extensionality, as well as how to reconcile instantiation techniques with functional variables. I’ll also present an evaluation showing that the implementations in veriT and cvc4 are competitive with state-of-the-art HOL provers and often outperform the traditional encoding into FOL.
Titouan Carette
Flexsymmetry, flexcyclicity, will they bend? #T4
In some cases (for example in quantum computing), we can grasp new insight on processes by representing them diagrammatically. To do so, we use graphical languages. Among them, the ZX-calculus enjoys a very nice property: diagrams can be thought up as graphs. This phenomenon is referred as the Only Topology Matters paradigm. Where does this property come from ? How to axiomatize it ? What role can it play in graphical language design ? This talk will investigate those questions.
Bizhan Alipourpijani
Inferring the gender of Facebook picture owners #T5
Social media such as Facebook provides a new way to connect, interact and learn. Facebook allows users to share photos and express their feelings by using comments. However, Facebook users arevulnerable to attribute inference attacks where an attacker intends to guess private attributes (e.g., gender, age, political view) of target users through their online profiles and/or theirvicinity (e.g., what their friends reveal). Given user-generated pictures on Facebook, we explore in our work how to launch gender inference attacks on their owners from pictures meta-datacomposed of: (i) alt-texts generated by Facebook to describe the content of pictures, and (ii) comments posted by friends, friends of friends or regular users. We assume these two meta-data arethe only available information to the attacker. Evaluation results demonstrate that our attack technique can infer the gender with an accuracy of 84% by leveraging only alt-texts, 96% by usingonly comments, and 98% by combining alt-texts and comments. We compute a set of sensitive words that enable attackers to perform effective gender inference attacks. We show the adversaryprediction accuracy is decreased by hiding these sensitive words. To the best of our knowledge, this is the first inference attack on Facebook that exploits comments and alt-texts solely.
12h30-14h00 : Lunch
Session 3 : 14h-16h
Charlie Jacomme
Decision problems on probabilistic programs over finite fields #T6
Questions about probabilistic programs over finite fields arise naturally for instance in the field of security. For verification purposes, one may wish to prove for instance the equivalence of programs, or the independance of some expressions. For programs without loops and given a finite field, we provide the exact complexity of some of those questions. Moreover, an interesting question also arises from the field of security. Indeed, cryptographers sometimes expects a property to hold for all extensions of a finite field. For instance, one could want to prove that two programs are equivalent for all possible length of bitstrings. We study the decidability of the previous questions in this new setting, notably proving the decidability in the case of equivalence.
Robert Booth
Flow Conditions for Continuous Variable Measurement-based Quantum Computation #T7
We introduce flow-based methods for continuous variables graph states, inspired by the notions of flow and g-flow for discrete variables measurement-based quantum computing first introduced byDanos and Kashefi and Browne et al. This allows us to formulate a protocol for measurement-based quantum computing in continuous variables using generic entanglement topologies. Furthermore, we give anecessary and sufficient condition for these protocols to converge in the limit of infinite squeezing and perfect measurements. Like for discrete variables, these constructions are useful fordetermining when an arbitrary CV graph state can be used for a practical computation.
Itsaka Rakotonirina
Efficient verification of observational equivalences in finite-process calculi #T8
Cryptographic protocols are concurrent programs aiming at offering security guarantees such as authentication or privacy while communicating through unreliable networks such as the Internet. For computer-aided verification, privacy is often modelled as observational equivalences in concurrent process calculi, that are undecidable in general. By bounding the number of protocol participants,it is possible to obtain decidability under some assumptions on the cryptographic primitives used by the protocol. We provide optimisation techniques for this decision problem (that has a high worst-case computational complexity), and implement them in a state-of-the-art automated tool. We also study to which extent these proofs (i.e. for a fixed number of participants) cangeneralise to the unbounded case in the case of electronic voting.
Alexis Grall
Integration of Event-B and Distalgo #T9
Distributed systems are known to be hard to design and verify. Refinement techniques have been successfully used to design correct models of distributed systems. The Event-B method uses refinement for designing correct-by-construction systems with tools for translating Event-B models into programs. However, these tools are not designed for distributed algorithms. We defined some constraints for modelling Event-B distributed algorithms which enable the translation of such an Event-B model into a program. I will use an example of a simple distributed algorithm to illustrate the constraints and a translation in DistAlgo. DistAlgo is a high level programming language based on Python for distributed algorithms.
