Midwest Verification Day 2012 Info
 Share
The version of the browser you are using is no longer supported. Please upgrade to a supported browser.Dismiss

 
View only
 
 
Still loading...
ABDEGHIJKLMNOPQRSTU
1
Day 1Time
2
8:30 AMCoffee
3
8:50 AMWelcome
4
Session 19:00 AMNatural Proofs for Structure, Data, and Separation Xiaokang Qiu
5
9:25 AMA Monadic Confinement CalculusAdam Procter
6
9:50 AMDesign and Checking of Conditional Information Flow Contracts Zhi Zhang and John Hatcliff
7
10:15 AMBreak
8
Session 210:30 AMThe HERMIT in the TreeNeil Sculthorpe, Andrew Farmer and Andy Gill
9
10:55 AMCompositional and Lightweight Dependent Type Inference for ML He Zhu and Suresh Jagannathan
10
11:20 AMProof Pad: An Integrated Development Environment for ACL2 Caleb Eggensperger
11
11:45 AMLunch
12
Session 31:00 PMA Do-It-Yourself High-Assurance CompilerLee Pike
13
2:00 PMBreak
14
Session 42:15 PMVerifying Lambda-Calculus Abstract Machines in Trellys Angello Astorga, Aaron Stump, Peng Fu and Garrin Kimmell
15
2:40 PMPlugging Resource Leaks With Path-Sensitive Heap Reachability Analysis Sam Blackshear, Bor-Yuh Evan Chang and Manu Sridharan
16
3:05 PMDependent Lambda Encodings in Selfstar Aaron Stump and Peng Fu
17
3:30 PMBreak
18
Session 53:45 PMParallelizing solvers for effectively propositional problems Tianyi Liang and Cesare Tinelli
19
4:10 PMThe Abella Approach to Specifying and Reasoning about Formal Systems Yuting Wang and Gopalan Nadathur
20
4:35 PMWhat's New in Formal Verification at Rockwell Collins? David Hardin and Raymond Richards
21
5:00 PMClose
22
23
24
Day 2
25
8:30 AMCoffee
26
8:50 AMAnnouncements
27
Session 69:00 AMGenerating Small Countermodels Using SMT Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstic
28
9:25 AMEPR-Based Bounded Model Checking at Word Level Christoph Sticksel
29
9:50 AMMinimum satisfying assignments for SMT using Bron-Kerbosch algorithm Tuan-Hung Pham, Michael Whalen and Sanjai Rayadurgam
30
10:15 AMBreak
31
Session 710:30 AMObservable Modified Condition/Decision Coverage Michael Whalen, Gregory Gay, Dongjiang You, Mats Heimdahl and Matt Staats
32
10:55 AMInferring Invariants for Dictionaries Arlen Cox, Bor-Yuh Evan Chang and Sriram Sankaranarayanan
33
11:20 AMModular Reflection Checking with Relationship Refinements Devin Coughlin and Bor-Yuh Evan Chang
34
11:45 AMLunch
35
Session 81:00 PMHereditary Substitution for the lambda-Delta-Calculus Harley Eades
36
1:25 PMHybrid Shape Analysis Yi-Fan Tsai and Bor-Yuh Evan Chang
37
1:50 PMTimed Relational Abstractions For Sampled Data Control Systems Aditya Zutshi
38
2:15 PMBreak
39
Session 82:30 PMTowards a Verified Trusted Platform ModuleBrigid Halling and Perry Alexander
40
2:55 PMPiecewise Linear Modeling of Nonlinear Devices for Formal Verification of Analog Circuits Yan Zhang, Sriram Sankaranarayanan and Fabio Somenzi
41
3:20 PMProtect & Serve: A Mechanism for Policing Soundness of Compile-Time ProofEvan Austin and Perry Alexander
42
3:45 PMClose
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
Loading...
 
 
 
Schedule
Submissions