PAS 2013
Tentative Schedule
Wednesday
23rd October
|
|
Chair: Wei Li |
|
09:00-09:25 |
Opening |
|
09:30-10:15 |
Deepak Kapur: A Logic for Parameterized
Octagonal Constraints with ±∞ |
|
10:15-10:30 |
Break |
|
|
Chair: Deepak Kapur |
|
10:30-11:15 |
Nikolaj Bjørner: SMT for Network Verification |
|
11:20-12:05 |
Naijun Zhan: Formal Verification of Simulink
Diagrams |
|
12:10-14:00 |
Lunch |
|
|
Chair: Nikolaj Bjørner |
|
14:00-14:45 |
Tudor Jebelean:
Proof–Based Algorithm Synthesis: A Case Study on Sorting |
|
14:50-15:35 |
Fairouz Kamareddine: Types and Functions Since Principia and the Computerisation of Language and Mathematics |
|
15:35-15:50 |
Break |
|
|
Chair: Fairouz Kamareddine |
|
15:50-16:35 |
Alessandro Armando: Model Checking Programs with
Arrays |
|
16:40-17:25 |
Jin Song Dong: Pervasive Model Checking and
Event Analytics |
|
17:30-17:55 |
Anping He and Jinzhao Wu: Asynchronous Circuit —
Design and Verification |
|
18:15- |
Reception |
Thursday 24th October
|
|
Chair: Dongming Wang |
|
09:00-09:45 |
Stephen M. Watt: The More
Symbolic the Better! |
|
09:50-10:35 |
Wolfgang Windsteiger: Theorema 2.0: An Open-Source Mathematical Assistant
System for Automated and Interactive Reasoning |
|
10:35-10:50 |
Break |
|
|
Chair: Stephen M. Watt |
|
10:50-11:35 |
Kaile Su: A New Efficient
OBDD Package with Dynamic Cache Management |
|
11:40-12:05 |
Wei Li and Dongchen Jiang:
Revision with Possibility |
|
12:10-15:20 |
Lunch + Hiking |
|
|
Chair: Wolfgang
Windsteiger |
|
15:20-16:05 |
Dorel Lucanu: Symbolic
Execution in K Framework: Support and Applications |
|
16:10-16:35 |
Jie Luo and Wei Li: R-calculus on
Description Logic |
|
16:35-16:50 |
Break |
|
|
Chair: Dorel Lucanu |
|
16:50-17:35 |
Adel Bouhoula: An Overview
of Proof by Induction for Algebraic Specifications |
|
17:40-18:05 |
He Li and Mengxiang Lin: Locating and
Understanding Concurrency Bugs Based on Edge-labeled Communication Graphs |
|
18:15- |
Dinner |
Friday 25th October
|
|
Chair: Tudor Jebelean |
|
09:00-09:45 |
Jens Knoop, Laura Kovács, and Jakob Zwirchmayr: Replacing Conjectures by Positive Knowledge:
Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic
Execution |
|
09:50-10:35 |
Marius Minea: A Symbolic
Execution Approach for Python Programs |
|
10:35-10:50 |
Break |
|
|
Chair: Jens Knoop |
|
10:50-11:35 |
Boris Konev: Clausal Temporal Resolution |
|
11:40-12:05 |
Xingyuan Zhang and Christian Urban: Turing Machines and
Separation Logic: Formalising Computability Theory
in the Isabelle/HOL Theorem Prover |
|
12:10-14:00 |
Lunch |
|
|
Chair: Boris Konev |
|
14:00-14:45 |
Wolfgang Schreiner: Applying Predicate Logic to Monitoring Network Traffic |
|
14:50-15:15 |
Hao Huang, Fangmin Song,
and Zhenjiang Qian: VTOS: A Finite State Machine Model
of OS and Formalized Verification of Its Microkernel |
|
15:20-15:40 |
Closing |