This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
malta13 [2013/06/16 19:02]
malta13 [2014/09/17 11:03] (current)
Line 12: Line 12:
 === Sunday, 16 June 2013 === === Sunday, 16 June 2013 ===
-| 10.00-10.30 | //Christian Colombo:// Verifying Web Applications:​ From Business Level Specifications to Automated Model-Based Testing | + 
-| 10.30-11.00 | //Julian Samborski-Forlese:// TBA +^             ^ Title                 ^ Speaker ^ 
-| 11.00-11.30 | **Coffee break** | +| 10.00-10.30 | {{:malta13-colombo.pptx|Verifying Web Applications:​ From Business Level Specifications to Automated Model-Based Testing}} | Christian Colombo ​
-| 11.30-12.00 | //Tarmo Uustalu:// ​Coinductive big-step semantics for concurrency | +| 10.30-11.00 | {{:​malta13-samborski-forlese.pdf|Simulation Relations for Rich Acceptance Conditions}} | Julian Samborski-Forlese | 
-| 12.00-12.30 | //Enric Rodriguez-Carbonell:// To Encode or to Propagate? The Best Choice for Each Constraint in SAT | +| 11.00-11.30 | **Coffee break** ​|
-| 12.30-14.00 | **Lunch** | +| 11.30-12.00 | Coinductive big-step semantics for concurrency ​| Tarmo Uustalu ​
-| 14.00-14.30 | //Tayssir Touilli:// ​Model-checking for efficient malware detection ​+| 12.00-12.30 | {{:malta13-rodriguez-carbonell.pdf|To Encode or to Propagate? The Best Choice for Each Constraint in SAT}} | Enric Rodriguez-Carbonell ​
-| 14.30-15.00 | //Guillermo Perez:// Decidable Classes of Mean-Payoff Games with Imperfect Information | +| 12.30-14.00 | **Lunch** ​|
-| 15.00-15.30 | **Coffee break** | +| 14.00-14.30 | Model-checking for Efficient Malware Detection | Tayssir Touilli ​
-| 15.30-16.00 | //Gordon Pace:// Contract Analysis ​+| 14.30-15.00 | {{:malta13-perez.pdf|Decidable Classes of Mean-Payoff Games with Imperfect Information}} | Guillermo Perez 
-| 16.00-16.30 | //Jonas Jensen:// Fictional Separation Logic | +| 15.00-15.30 | **Coffee break** ​|
-| 16.30-17.30 | MC Meeting | +| 15.30-16.00 | {{:​malta13-pace.pdf|Reasoning About Contracts}} | Gordon Pace | 
-| 19.30- | **Workshop dinner** |+| 16.00-16.30 | {{:malta13-jensen.pdf|Fictional Separation Logic}} | Jonas Jensen ​
 +| 16.30-17.30 | MC Meeting ​|
 +| 19.30- | **Workshop dinner** ​||
 === Monday, 17 June 2013 === === Monday, 17 June 2013 ===
-| 09.00-10.00 | Invited Speaker**Manuel Hermenegildo** +^             ^ Title                 ^ Speaker ^ 
-| 10.00-10.30 | **Coffee break** | +| 09.00-10.00 | {{:​malta13-hermenegildo.pdf|Analysis and Verification ``of and with''​ Horn Clauses (using the Ciao system) }}**(Invited Speaker)** Manuel Hermenegildo | 
-| 10.30-11.00 | //Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses | +| 10.00-10.30 | **Coffee break** ​|
-| 11.00-11.30 | //Boriss Selajev:// Scaling ​dynamic logic for intermediate states ​+| 10.30-11.00 | {{:malta13-beyene.pdf|Solving Existentially Quantfied Horn Clauses}} | Tewodros Beyene ​
-| 11.30-12.00 | //Ondrej Lengal:// Fully Automated Shape Analysis Based on Forest Automata | +| 11.00-11.30 | {{:malta13-selajev.pdf|Scaling ​Dynamic Logic for Intermediate States}} | Boriss Selajev ​
-| 12.00-12.30 | //Alejandro Sanchez:// Invariant Generation for Parametrized Systems using Self-Reflection | +| 11.30-12.00 | {{:malta13-lengal.pdf|Fully Automated Shape Analysis Based on Forest Automata}} | Ondrej Lengal ​
-| 12.30-14.00 | **Lunch** | +| 12.00-12.30 | {{:malta13-sanchez.pdf|Invariant Generation for Parametrized Systems using Self-Reflection}} | Alejandro Sanchez ​
-| 14.00-15.00 | Invited speaker**John Gallagher** +| 12.30-14.00 | **Lunch** ​|
-| 15.00-15.30 | **Coffee break** | +| 14.00-15.00 | {{:​malta13-gallagher.pdf|Verification by Abstraction and Specialisation of Constraint Logic Programs}} **(Invited speaker)** John Gallagher | 
-| 15:30-16:00 | //Siirtola Antti:// Object-Oriented Programs as Parameterised Systems | +| 15.00-15.30 | **Coffee break** ​|
-| 16.00-16.30 | //Filip Konecni:// Underapproximation of Procedure Summaries for Integer Programs | +| 15:30-16:00 | {{:malta13-siirtola.pdf|Object-Oriented Programs as Parameterised Systems}} | Siirtola Antti 
-| 16.30-17.00 | //Paul Jackson:// Auditing User-provided Axioms in Software Verification Conditions | +| 16.00-16.30 | {{:malta13-konecny.pdf|Underapproximation of Procedure Summaries for Integer Programs}} | Filip Konecni ​
-| 17:00-17:30 | Discussion Session: Cross-fertilization between Logic Programming ​and CLP with Horn Clause Verification |+| 16.30-17.00 | {{:malta13-jackson.pdf|Auditing User-provided Axioms in Software Verification Conditions}} | Paul Jackson ​
 +| 17:​00-17:​30 ​| {{:​malta13-monniaux.pdf|Death by a Thousand Cuts (worst-case execution time by bounded model checking)}} | David Monniaux | 
 +| 17:​30-18:​00 ​| Discussion Session: Cross-fertilization between Logic Programming with CLP and Horn Clause Verification ​||
 ===== General Information ===== ===== General Information =====
Line 98: Line 102:
   * **High-level synthesis:​** New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections ​ between invariant generation and code synthesis.   * **High-level synthesis:​** New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections ​ between invariant generation and code synthesis.
-===== Talk Abstracts ====+===== Talk Abstracts ====
 +**Verifying Web Applications:​ From Business Level Specifications to Automated Model-Based Testing** 
 +//Christian Colombo// 
 +While the verification of web-based applications is crucial due to their often security-critical nature, it is considerably challenging due to their complex and dynamical nature. The current state of the art involves automated test execution where a test platform automatically interacts with a web application and asserts the expected behaviour. Still, test cases are typically generated manually, particularly when it comes to directing the test to exercise particular execution paths. In this presentation,​ we propose a novel combination of the QuickCheck testcase generation tool with web-based applications:​ QuickCheck exploits an executable automata-based specification to drive and assert the application in an automated yet non-random fashion. However, writing the specification is non-trivial and requires manual intervention. To this end, we propose a means of generating QuickCheck specifications from Cucumber specifications – a commonly used high level specification language for communicating with business stakeholders.  
 +** Simulation Relations for Rich Acceptance Conditions ** 
 +//Julian Samborski-Forlese//​ 
 +Antichain algorithms allow to obtain faster emptiness and model checking 
 +algorithms for alternating automata by postponing the state explosion 
 +inherent to the translation into equivalent non-deterministic automata. 
 +Antichains require computable simulation relations between sets of states in 
 +the alternating automaton which depend on the acceptance condition. So far, 
 +only Buchi conditions have been studied, which preclude the application of 
 +antichains to rich temporal logics like RLTL and PSL, for which more 
 +sophisticated acceptance conditions are used. In this talk we present 
 +simulation relations for some Rabin and Streett automata that enable the use 
 +of antichains for these richer temporal logics 
 +** Coinductive big-step semantics for concurrency ** 
 +//Tarmo Uustalu//  
 +Going against the popular statements that big-step semantics cannot handle ​      
 +nontermination (they would necessarily "​lose"​ all nonterminating runs) and       
 +that concurrency is inherently small-step, I present a big-step semantics ​       
 +for shared-variable concurrency that accounts correctly for both                 
 +terminating and nonterminating runs. This semantics is based on                  
 +coinductive and mixed inductive-coinductive definitions of resumptions ​          
 +(computation trees), evaluation and termination-sensitive weak                   
 +bisimilarity. Big-step reasoning offers a higher degree of                       
 +compositionality as is exemplified eg by rely-guarantee style program ​           
 +logics that are in fact big-step and are more directly matched with              
 +big-step rather than small-step semantics. I develop the metatheory of the       
 +semantics in a constructive logic. ​                                              
 +** To Encode or to Propagate? The Best Choice for Each Constraint in SAT ** 
 +//Enric Rodriguez-Carbonell//​  
 +Sophisticated compact SAT encodings exist for many types of                      
 +constraints. Alternatively,​ for instances with many (or large) ​                  
 +constraints,​ the SAT solver can also be extended with built-in ​                  
 +propagators (the SAT Modulo Theories approach, SMT).  For                        
 +example, given a cardinality constraint x_1 + ... + x_n <=                 
 +k, as soon as k variables become true, such a propagator can                  
 +set the remaining variables to false, generating a so-called ​                    
 +explanation clause of the form x_1 /\ .../\ x_k                       
 +-> ~ x_i.  But certain "​bottle-neck"​ constraints ​                 
 +end up generating an exponential number of explanations, ​                        
 +equivalent to a naive SAT encoding, much worse than using a                      
 +compact encoding with auxiliary variables from the beginning. ​                   
 +Therefore, Abio and Stuckey proposed starting off with a full                
 +SMT approach and partially encoding, on the fly, only                     
 +certain ``active''​ parts of constraints. ​ Here we build upon                     
 +their work.                                                                      
 +Equipping our solvers with some additional bookkeeping to monitor ​               
 +constraint activity has allowed us to shed light on the                          
 +effectiveness of SMT: many constraints generate very few, or few                 
 +different, explanations. ​                                                        
 +We also give strong experimental evidence showing that it is typically 
 +unnecessary to consider partial encodings: it is competitive to encode 
 +the few really active constraints entirely. This makes the approach 
 +amenable to any kind of constraint, not just the ones for which 
 +partial encodings are known. 
 +This is joint work with Ignasi Abío, Robert Nieuwenhuis,​ Albert ​                 
 +Oliveras and Peter J. Stuckey. ​                                                  
 +** Model-checking for efficient malware detection ** 
 +//Tayssir Touilli//  
 +The number of malware is growing extraordinarily fast. Therefore, it is          
 +important to have efficient malware detectors. Malware writers try to            
 +obfuscate their code by different techniques. Many of these well-known ​          
 +obfuscation techniques rely on operations on the stack such as inserting ​        
 +dead code by adding useless push and pop instructions,​ or hiding calls           
 +to the operating system, etc. Thus, it is important for malware ​                 
 +detectors to be able to deal with the program’s stack. In this paper we          
 +propose a new model-checking approach for malware detection that takes           
 +into account the behavior of the stack. Our approach consists in : (1)           
 +Modeling the program using a Pushdown System (PDS). (2) Introducing new          
 +logics, called SCTPL and SLTPL, to represent the malicious behavior. ​            
 +SCTPL (resp. SLTPL) can be seen as an extension of the branching-time ​           
 +temporal logic CTL (resp. the linear-time temporal logic LTL) with               
 +variables, quantifiers,​ and predicates over the stack. (3) Reducing the          
 +malware detection problem to the model-checking problem of PDSs against ​         
 +SCTPL/SLTPL formulas. We show how our new logics can be used to                  
 +precisely express malicious behaviors that could not be specified by             
 +existing specification formalisms. We then consider the model-checking ​          
 +problem of PDSs against SCTPL/SLTPL specifications. We provide efficient ​        
 +algorithms to solve these problems. We implemented our techniques in a           
 +tool, and we applied it to detect several viruses. Our results are               
 +encouraging. ​                                                                    
 +In particular, our tool was able to detect more than 800 viruses. ​               
 +Several of these viruses could not be detected by well-known ​                    
 +anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee. ​  
 +** Decidable Classes of Mean-Payoff Games with Imperfect Information ** 
 +//Guillermo Perez//  
 +Energy games and Mean-payoff games have been studied as two-player games         
 +with quantitative objectives. In the perfect information setting deciding ​       
 +the winner of such games is known to be in both NP and coNP yet only             
 +pseudo-polynomial time algorithms have been found for the                        
 +original unmodified objectives. The problem of determining if an energy ​         
 +game with imperfect information has a winning strategy is known to be            
 +undecidable for the case when the initial credit is not fixed. The same is       
 +true for the problem of determining if a mean-payoff game with imperfect ​        
 +information has a winning strategy. We propose a new class of mean-payoff ​       
 +games with imperfect information for which the problem is known to be            
 +decidable and for which the aforementioned problem is EXPTIME-complete. We       
 +also consider the complexity of deciding if a given weighted game graph          
 +with imperfect information belongs to this class. In order to better ​            
 +understand the source of undecidability for these objectives under               
 +imperfect information we also consider related classes of weighted game          
 +graphs with imperfect information as well as the related class membership ​       
 +and existence of winning strategy problems. ​                                     
 +** Contract Analysis ** 
 +//Gordon J. Pace// 
 +The analysis of contracts to regulating interactive systems poses various challenges, but 
 +is closely linked to the notions of concurrency and synchrony. We present a number of 
 +recent results which take an automaton-based approach to model such contracts. We show how 
 +obligations,​ permissions and prohibitions can be formalised and how the norms on one of the 
 +parties sometimes imposes constraints on the other. Such formalisation allows for a clean 
 + ​notion of contract strictness and a derived notion of contract conflict that is enriched  
 +with issues arising from party interdependence. 
 +//Joint work with Fernando Schapachnik and Gerardo Schneider.//​ 
 +** Fictional Separation Logic ** 
 +//Jonas Jensen// 
 +** ** 
 +//Manuel Hermenegildo//​ 
 +The talk will start with an overview of techniques for abstract 
 +interpretation-based program analysis and verification of constraint 
 +logic programs (CLP), with emphasis on the on top-down fixpoint 
 +algorithms used in the Ciao system (note that bottom-up techniques 
 +will be covered in John Gallagher'​s talk). ​ We will demonstrate the 
 +Ciao system analysis and verification-based program development 
 +environment,​ built around these techniques and capable of verifying 
 +shapes, modes, determinacy,​ non-failure,​ numerical properties, etc. as 
 +well as resources such as bandwidth, time, memory, or, more recently, 
 +energy. We will then address how, by using CLP as an intermediate 
 +representation,​ the approach (and the Ciao system itself) also 
 +supports the verification of similar properties in programs in other 
 +programming paradigms, including Java source or bytecode, and assembly 
 +code produced from C sources. ​ Finally, we present how the same 
 +fixpoint techniques are applied in the execution of Tabled LP programs 
 +(such as in the XSB system) and Tabled CLP programs (such as in the 
 +TCLP package of the Ciao system), which can be an interesting 
 +component for program analyzers for other programming paradigms. 
 +** Solving Existentially Quantfied Horn Clauses ** 
 +//Tewodros Beyene// 
 +Temporal verification of universal (i.e., valid for all computation paths) 
 +properties of various kinds of programs, e.g., procedural, multi-threaded,​ 
 +or functional, can be reduced to finding solutions for equations in form of 
 +universally quantified Horn clauses extended with well-foundedness 
 +conditions. Dealing with existential properties (e.g., whether there exists 
 +a particular computation path), however, requires solving forall-exists 
 +quantified Horn clauses, where the conclusion part of some clauses contains 
 +existentially quantified variables. For example, a deductive approach to 
 +CTL verification reduces to solving such clauses. 
 +The talk presents a method for solving forall-exists quantified Horn 
 +clauses extended with well-foundedness conditions. Our method is based on a 
 +counterexample-guided abstraction refinement scheme to discover witnesses 
 +for existentially quantified variables. We also present an application of 
 +our solving method to automation of CTL verification of software, as well 
 +as its experimental evaluation. 
 +** Scaling dynamic logic for intermediate states ** 
 +//Boriss Selajev//  
 +Standard sequential program logics are insufficient for reasoning ​               
 +about nonterminating program runs --- they essentially overlook them.            
 +But of course we want to reason also about nonterminating behaviors, ​            
 +especially in case of interactive programs. To remedy this deficiency, ​          
 +we are interested in identifying a useful extension of dynamic logic             
 +with modalities for predicating not only final, but also intermediate ​           
 +states of program runs. In this talk, I discuss some possible designs ​           
 +for such a program logic on the level of syntax, semantics and                   
 +prospective axiomatizations. (Joint work with Keiko Nakata and Tarmo             
 +Uustalu.) ​                                                                       
 +** Fully Automated Shape Analysis Based on Forest Automata ** 
 +//Ondrej Lengal//  
 +Forest automata (FA) have recently been proposed as a tool                     
 +for shape analysis of complex heap structures. FA encode sets of               
 +tree decompositions of heap graphs in the form of tuples of tree               
 +automata. In order to allow for representing complex heap graphs, ​             
 +the notion of FA allowed one to provide user-defined FA (called ​               
 +boxes) that encode repetitive graph patterns of shape graphs to be             
 +used as alphabet symbols of other, higher-level FA. In this paper, ​            
 +we propose a novel technique of automatically learning the FA to be            
 +used as boxes that avoids the need of providing them manually. ​                
 +Further, we propose a significant improvement of the automata ​                 
 +abstraction used in the analysis. The result is an efficient, ​                 
 +fully-automated analysis that can handle even as complex data                  
 +structures as skip lists, with the performance comparable to                   
 +state-of-the-art fully-automated tools based on separation logic, ​             
 +which, however, specialise in dealing with linked lists only.                  
 +** Invariant Generation for Parametrized Systems using Self-Reflection ** 
 +//Alejandro Sanchez//  
 +We examine the problem of inferring invariants for parametrized systems. 
 +Parametrized systems are concurrent systems consisting of an a priori 
 +unbounded number of process instances running the same program. Such 
 +systems are commonly encountered in many situations including device 
 +drivers, distributed systems, and robotic swarms. In this talk, I will 
 +describe a technique that enables leveraging off-the-shelf invariant 
 +generators designed for sequential programs to infer invariants of 
 +parametrized systems. The central challenge in invariant inference for 
 +parametrized systems is that naïvely exploding the transition system with 
 +all interleavings is not just impractical but impossible. In our approach, 
 +the key enabler is the notion of a reflective abstraction that we prove has 
 +an important correspondence with inductive invariants. This correspondence 
 +naturally gives rise to an iterative invariant generation procedure that 
 +alternates between computing candidate invariants and creating reflective 
 +This is joint work with Sriram Sankaranarayanan,​ César Sánchez and Bor-Yuh 
 +Evan Chang. 
 +** Verification by abstraction and specialisation of constraint logic programs ** 
 +//John Gallagher//​ 
 +This talk addresses the question of how static analysis and verification 
 +techniques for constraint logic programs (CLP) are applied to other 
 +formalisms. ​ First, the systematic translation of a variety of languages and 
 +systems to constraint logic programs is reviewed, using the established 
 +method of partial evaluation of semantics, proof rules and assertions 
 +represented as CLP meta-programs. Then the approximation of CLP programs 
 +using abstract interpretation is described, with implementation techniques 
 +using external engines to implement abstract domains. ​ Both numeric and 
 +symbolic abstract domains (tree automata) are considered. The talk focusses 
 +on verification based on approximation of program models (bottom-up 
 +semantics) rather than the alternative approach based on computation-tree 
 +operational semantics. The role of so-called "magic set" transformations and 
 +related techniques originating in Datalog is presented, enabling 
 +query-directed analysis in the same bottom-up framework. Analysis for proof 
 +of termination is also briefly reviewed. Thirdly, program transformations 
 +that preserve CLP models are presented; this leads to verification 
 +approaches in which a CLP program is successively specialised with respect 
 +to a query until the property of interest is made explicit. ​ Finally we look 
 +at abstract model checking based on CLP.  By applying standard abstract 
 +interpretation techniques it is shown how arbitrary CTL properties can be 
 +approximated without resorting to "​dual"​ or "​modal"​ transition systems. 
 +** Object-Oriented Programs as Parameterised Systems ** 
 +//Siirtola Antti// 
 +Object-oriented programs possess many parameters like the number of concurrent 
 +threads, the number of replicated objects and the number of nested function 
 +calls. Consequently,​ object-oriented programs are naturally modelled as 
 +multi-parameterised systems. In this talk, I present one way to model Java-like 
 +programs as parameterised systems in a CSP-style formalism. I also show how such 
 +parameterised models can be automatically model checked by utilising existing 
 +**  Underapproximation of Procedure Summaries for Integer Programs ** 
 +//Filip Konecni// 
 +We show how to underapproximate the procedure summaries of recursive ​            
 +programs over the integers using off-the-shelf analyzers for                     
 +non-recursive programs. The novelty of our approach is that the                  
 +non-recursive program we compute may capture unboundedly many behaviors ​         
 +of the original recursive program for which stack usage cannot be                
 +bounded. Moreover, we identify a class of recursive programs on which            
 +our method terminates and returns the precise summary relations without ​         
 +underapproximation. Doing so, we generalize a similar result for                 
 +non-recursive programs to the recursive case. Finally, we present ​               
 +experimental results of an implementation of our method applied on a             
 +number of examples. 
 +** Auditing User-provided Axioms in Software Verification Conditions ** 
 +//Paul Jackson// 
 +Sometimes software verification conditions (VCs) include user-provided 
 +axioms to capture aspects of program specifications or to give hints 
 +to help automatic provers. There is always the danger of mistakes in 
 +these axioms. In the worst case these mistakes introduce 
 +inconsistencies and VCs become erroneously provable. 
 +I'll discuss use of an SMT solver to investigate the quality of 
 +user-provided axioms employed in the formal verification of SPARK-Ada 
 +** TBD ** 
 +//David Monniaux//
 +===== Group Photo =====
 +Group picture in Mdina, Malta: