VSL 2014: VIENNA SUMMER OF LOGIC 2014
CAV ON FRIDAY, JULY 18TH, 2014
Days:
previous day
next day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 86B: Tutorial: How do we get inductive invariants?
Location: FH, Hörsaal 6
08:45
How do we get inductive invariants? (Part A)

ABSTRACT. Verifying the correctness of loop-free programs (or of general programs, up to bounded depth) is difficult: the state space explodes exponentially as the depth increases. Yet, the difficulty increases as we allow unboundedly many execution steps; proof approaches then generally rely on finding inductive invariants (properties shown to hold initially, then to remain true by induction).

Abstract interpretation attempts finding inductive invariants within a given domain, e.g. conjunctions of linear inequalities. The classical approach iterates a transformer until the property becomes inductive. In general, this approach may not terminate; thus termination is often enforced with a “widening” operator, which attempts at generalizing the iterates into an inductive property. Unfortunately, widening operators are brittle, with non-monotonic behaviors (supplying more information about a system may result in worse analysis outcomes!). Therefore, other approaches have been developed (policy iteration,…), which avoid this pitfall.

Finally, we shall discuss possible combinations of abstract interpretation and SMT-solving.

09:00-18:00 Session 87D: FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (joint with 9 other meetings)
Location: EI, Foyer
09:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
SPEAKER: unknown

ABSTRACT. OWL is a logic-based ontology language standard designed to promote interoperability, particularly in the context of the (Semantic) Web. The standard has encouraged the development of numerous OWL reasoning systems, and such systems are already key components of many applications. The 2nd OWL Reasoner Evaluation Competition (ORE 2014) compares and evaluates 11 OWL reasoning systems on a data set containing a wide range of ontologies from the web, obtained through a standard web crawl and the Google Custom Search API, and a snapshot from the well known BioPortal repository. Some user submitted ontologies spice up the corpus with particularly relevant and difficult test cases. The ontologies in the test set are binned by profiles to enable the participation of reasoners specialised on the EL and DL profiles of OWL. The evaluation is performed in three different categories that cover the important tasks of ontology classification, consistency checking, and ontology realisation (i.e., the computation of entailed types of individuals).

09:00-18:00 Session 87E: FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (joint with 9 other meetings)
Location: FH, 2nd floor
09:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
SPEAKER: unknown

ABSTRACT. The 9th SMT competition seeks to spur interest, usefulness, and capability of SMT solvers in application-centric contexts. This year's competition has 20 solvers from 14 participating teams (a record number) with problems drawn from 147K benchmarks in 34 different logics; problems are expressed in a common, standardized format (SMTLIBv2). There are tracks measuring sequential and parallel performance and emulating batch and interactive application environments. The benchmarks are increasingly supplied by application environments that use SMT solvers to discharge constraint problems and verification conditions that arise in software verification, scheduling, component placement and other domains. The competition is run over a period of a month using the StarExec computation cluster. This year there is also a separate, experimental sibling competition on Separation Logic solvers and problems, also using the concrete syntax of SMTLIBv2 benchmarks.

10:15-10:45Coffee Break
10:45-12:15 Session 90AD: Tutorial: How do we get inductive invariants?
Location: FH, Hörsaal 6
10:45
How do we get inductive invariants? (Part B)

ABSTRACT. Verifying the correctness of loop-free programs (or of general programs, up to bounded depth) is difficult: the state space explodes exponentially as the depth increases. Yet, the difficulty increases as we allow unboundedly many execution steps; proof approaches then generally rely on finding inductive invariants (properties shown to hold initially, then to remain true by induction).

Abstract interpretation attempts finding inductive invariants within a given domain, e.g. conjunctions of linear inequalities. The classical approach iterates a transformer until the property becomes inductive. In general, this approach may not terminate; thus termination is often enforced with a “widening” operator, which attempts at generalizing the iterates into an inductive property. Unfortunately, widening operators are brittle, with non-monotonic behaviors (supplying more information about a system may result in worse analysis outcomes!). Therefore, other approaches have been developed (policy iteration,…), which avoid this pitfall.

Finally, we shall discuss possible combinations of abstract interpretation and SMT-solving.

13:00-14:30Lunch Break
14:30-16:00 Session 96AD: Tutorial: Hardware Model Checking
Location: FH, Hörsaal 6
14:30
Hardware Model Checking (Part A)
SPEAKER: Fabio Somenzi
16:00-16:30Coffee Break
16:30-18:00 Session 99AB: Tutorial: Hardware Model Checking
Location: FH, Hörsaal 6
16:30
Hardware Model Checking (Part B)
SPEAKER: Fabio Somenzi