VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR WEDNESDAY, JULY 23RD: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

ARW-DT
GeTFun
VeriSure
VERIFY
RS
ARQNL
WING
PAAR
FRIDA
Vampire
ASPOCP
SYNT
HSB
KR
PRUV
9:00
9:30
10:00
10:30
11:00
11:30
12:00
12:30
13:00
13:30
14:00
14:30
15:00
15:30
16:00
16:30
17:00
17:30
18:00
18:30
19:00
19:30
20:00
08:45-09:30
Stochastic Lambda Calculus - An Appeal
Dana Scott
09:30-10:15
Contracts for System Design
Albert Benveniste
08:45-09:15
Balancing the Formal and Informal in Safety Case Arguments
Tim Kelly, Ibrahim Habli
09:15-09:45
Quantification of Verification Progress
Stephan Arlt, John Murray, Philipp Ruemmer, Martin Schäf
08:45-09:45
Synthetic Systems Biology
Calin Guet
09:45-10:15
FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian
Donal Stewart, Stephen Gilmore, Michael Cousin
08:45-09:15
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Sophie Tourret, Mnacho Echenim, Nicolas Peltier
09:15-10:15
Invited talk: Hierarchic Superposition Revisited
Uwe Waldmann
08:45-09:30
From display logic to nested sequents via residuated frames
Nick Galatos
09:30-10:15
First-order non-classical logics: an order-based approach
Petr Cintula
08:45-09:45
Chasing the Perfect Specification
Carsten Schürmann
09:45-10:15
Typed First-Order Logic
Peter Schmitt, Mattias Ulbrich
08:45-09:45
Chasing the Perfect Specification
Carsten Schürmann
09:45-10:15
Typed First-Order Logic
Peter Schmitt, Mattias Ulbrich
08:45-09:45
Chasing the Perfect Specification
Carsten Schürmann
09:45-10:15
Typed First-Order Logic
Peter Schmitt, Mattias Ulbrich
08:55-10:10
Automating Deductive Synthesis with Leon (Invited Talk)
Viktor Kuncak
08:55-09:00 Opening
09:00-10:15
Knowledge Representation Meets Computer Vision: From Pixels to Symbolic Activity Descriptions
Tony Cohn
09:00-10:15
Beyond Nash Equilibrium: Solution Concepts for the 21st Century
Joseph Halpern
09:00-09:15 Opening
09:10-09:25 Opening Remarks
09:15-10:15 Invited Talk
09:25-09:50
Supported Semantics for Modular Systems
Shahab Tasharrofi, Eugenia Ternovska
09:50-10:15
Infinitary Equilibrium Logic
Amelia Harrison, Vladimir Lifschitz, David Pearce, Agustín Valverde
09:45-10:15 Discussion
10:45-11:15
Stable Model Semantics for Guarded Existential Rules and Description Logics
Georg Gottlob, André Hernich, Clemens Kupke, Thomas Lukasiewicz
11:15-11:45
Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical
Michel Ludwig, Boris Konev
11:45-12:15
Nominal Schemas in Description Logics: Complexities Clarified
Markus Krötzsch, Sebastian Rudolph
12:15-12:45
Decidable Gödel Description Logics without the Finitely-Valued Model Property
Stefan Borgwardt, Felix Distel, Rafael Peñaloza
10:45-11:15
A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations
Fangzhen Lin
11:15-11:45
How To Progress Beliefs in Continuous Domains
Vaishak Belle, Hector Levesque
11:45-12:15
Transforming Situation Calculus Action Theories for Optimised Reasoning
Christopher Ewin, Adrian Pearce, Stavros Vassos
12:15-12:45
Forgetting in Action
David Rajaratnam, Hector Levesque, Maurice Pagnucco, Michael Thielscher
10:45-11:10
A Refinement of the Language of Epistemic Specifications
Michael Gelfond, Patrick Kahl, Richard Watson, Yuanlin Zhang
11:10-11:35
Epistemic Logic Programs with Sorts
Evgenii Balai, Patrick Kahl
10:45-11:30
A Geometric Model for Concurrent Programming
Tony Hoare
11:30-12:00
Automated Abstraction-Refinement for the Verification of Behavioral UML Models
Orna Grumberg
12:00-12:30
Probabilistic model checking at the nanoscale: from molecular signalling to molecular walkers
Marta Kwiatkowska
12:30-13:00
A Short Story on Scenarios
Shahar Maoz
10:45-11:15
Synthesis of a simple self stabilizing system
Adria Gascon, Ashish Tiwari
11:15-11:45
Program Synthesis and Linear Operator Semantics
Herbert Wiklicky
11:45-12:15
How to Handle Assumptions in Synthesis
Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, Robert Koenighofer
12:15-12:45
Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Aaron Bohy, Véronique Bruyère, Jean-Francois Raskin
10:45-12:00
First-Order Theorem Proving with Vampire
Laura Kovacs, Andrei Voronkov
12:00-12:30
Proofs in Vampire
Ashutosh Gupta
12:30-13:00
Playing with AVATAR
Giles Reger, Martin Suda, Andrei Voronkov
10:45-11:15
Introducing Semi-Formal Specifications into a Distributed Development Process
Hardi Hungar, Michael Meyer Zu Hörste
11:15-11:45
Witnessing an SSA Transformation
Kedar Namjoshi
10:45-11:30
Tutorial: Simulation-based Parameter Synthesis in Systems Biology
Alexandre Donze
11:30-12:00
Collaboration success stories: Modeling Iron Homeostasis in Mammalian Cells (with J.M. Moulis)
Eric Fanchon
12:00-12:30
Collaboration success stories: Control of Gene Expression in E.coli (with Hans Geiselman)
Hidde de Jong
12:30-13:00
Collaboration success stories: Membrane-bound Receptor Imaging, Data Analysis and Model Building (with J.S.
Adam Halasz
10:45-11:15
Automated Theorem Proving using the TPTP Process Instruction Language
Muhammad Nassar, Geoff Sutcliffe
11:15-11:45
The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
Negin Arhami, Geoff Sutcliffe
11:45-12:15
Machine Learner for Automated Reasoning 0.4 and 0.5
Cezary Kaliszyk, Josef Urban, Jiri Vyskocil
12:15-12:45
BliStr: The Blind Strategymaker
Josef Urban
10:45-11:15
Towards binary circuit models that faithfully reflect physical (un)solvability
Matthias Függer, Thomas Nowak, Ulrich Schmid, Robert Najvirt
11:15-11:45
Mechanical Verification of a Constructive Proof for FLP
Bisping et.al
11:45-12:15
Having SPASS with Pastry and TLA+
Noran Azmy
12:15-12:45
Concurrent Data Structures: Semantics and (Quantitative) Relaxation
Ana Sokolova
10:45-11:30
Broadly truth-functional logics through classical lenses
João Marcos
11:30-12:00
Natural deduction for non-deterministic finite-valued logics
Cecilia Englander, Hermann Hauesler
12:00-12:30
The procedural understanding of meaning and compositionality in formal semantics
Ivan Mikirtumov
12:30-13:00
Semi-BCI-algebras
Regivan Santiago, Benjamín Bedregal, João Marcos, Carlos Caleiro
10:45-11:15
Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Bernhard Beckert, Thorsten Bormer, Rajeev Gore, Michael Kirsten, Thomas Meumann
11:15-11:45
Introducing a Sound Deductive Compilation Approach
Ran Ji, Reiner Hähnle
11:45-12:15
Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?
Benja Fallenstein, Nate Soares
10:45-11:15
Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Bernhard Beckert, Thorsten Bormer, Rajeev Gore, Michael Kirsten, Thomas Meumann
11:15-11:45
Introducing a Sound Deductive Compilation Approach
Ran Ji, Reiner Hähnle
11:45-12:15
Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?
Benja Fallenstein, Nate Soares
10:45-11:15
Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Bernhard Beckert, Thorsten Bormer, Rajeev Gore, Michael Kirsten, Thomas Meumann
11:15-11:45
Introducing a Sound Deductive Compilation Approach
Ran Ji, Reiner Hähnle
11:45-12:15
Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?
Benja Fallenstein, Nate Soares
10:45-11:15
In Which Sense Is Fuzzy Logic a Logic for Vagueness?
Libor Behounek
11:15-11:45
Stable Models of Fuzzy Propositional Formulas
Joohyung Lee, Yi Wang
11:45-12:15
Towards a Logic of Dilation
Arina Britz, Ivan Varzinczak
10:50-11:00
ARQNL Workshop - Opening
Workshop Organizers
11:00-11:30
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Damein Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
11:30-12:00
A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
Ping Hou
12:00-12:30
Problem Libraries for Non-Classical Logics
Jens Otten, Thomas Raths
12:30-13:00
HOL Provers for First-order Modal Logics --- Experiments
Christoph Benzmüller
11:35-11:45 Short Break
11:45-12:10
Temporal Stable Models are LTL-representable
Pedro Cabalar, Martín Diéguez
12:10-12:35
Applying Action Language BC with Hierarchical Domain Abstraction to Mobile Robots
Shiqi Zhang, Fangkai Yang, Piyush Khandelwal, Peter Stone
12:35-13:00
Action Language BC+: Preliminary Report
Joseph Babb, Joohyung Lee
11:45-12:15 Discussion
12:15-12:45
Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED
P. Curzon, P. Masci, P. Oladimeji, R. Rukšėnas, H. Thimbleby, E. D'Urso
12:15-12:45
Reasoning about Auctions
Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat
12:45-13:15
Automating Regression Verification
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Mattias Ulbrich
12:15-12:45
Reasoning about Auctions
Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat
12:45-13:15
Automating Regression Verification
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Mattias Ulbrich
12:15-12:45
Reasoning about Auctions
Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat
12:45-13:15
Automating Regression Verification
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Mattias Ulbrich
14:30-15:00
Certain Answers as Objects and Knowledge
Leonid Libkin
15:00-15:30
Tackling Winograd Schemas by Formalizing Relevance Theory in Knowledge Graphs
Peter Schüller
15:30-16:00
Simultaneous Learning and Prediction
Loizos Michael
14:30-15:00
Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture
Mehul Bhatt, Carl Schultz, Madhura Thosar
15:00-15:30
Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge
Matthias Thimm
15:30-16:00
SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical
Andrea Marrella, Massimo Mecella, Sebastian Sardina
14:30-15:00
Quantitative Reactive Modeling
Thomas A. Henzinger
15:00-15:30
On Statecharts, Scenarios and Biological Modeling
Hillel Kugler
15:30-16:00
Cancer as Reactivity
Jasmin Fisher
14:30-15:30
My Life with an Automatic Theorem Prover
Jasmin Christian Blanchette
15:30-16:00
Discussions
Andrei Voronkov, Laura Kovacs
14:30-15:00
Proof Support for Common Logic
T. Mossakowski, M. Codescu, O. Kutz, C. Lange, M. Grüninger
15:00-15:30
Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
Max Wisniewski, Alexander Steen
15:30-16:00
Dialogues for proof search
Jesse Alama
14:30-15:00
Implicit Assumptions in a Model for Separation Kernels
Freek Verbeek, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Oto Havle
15:00-15:30
Assurance and Verification of Security Properties
Constance Heitmeyer
14:30-15:30
Tutorial: The Cellular Potts Model
Marco Antoniotti
15:30-16:00
Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
Tommaso Dreossi, Thao Dang, Carla Piazza
14:30-15:00
A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
Joshua Bax
15:00-15:30
Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Simon Cruanes
15:30-16:00
Polymorphic+Typeclass Superposition
Daniel Wand
14:30-15:45
On Checking Correctness of Concurrent Data Structures
Ahmed Bouajjani
14:30-15:00
A Theorem Prover Backed Approach to Array Abstraction
Nathan Wasser, Richard Bubel
15:00-15:30
ALICe: A Framework to Improve Affine Loop Invariant Computation
Vivien Maisonneuve, Olivier Hermant, François Irigoin
15:30-16:00
Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller
14:30-15:00
A Theorem Prover Backed Approach to Array Abstraction
Nathan Wasser, Richard Bubel
15:00-15:30
ALICe: A Framework to Improve Affine Loop Invariant Computation
Vivien Maisonneuve, Olivier Hermant, François Irigoin
15:30-16:00
Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller
14:30-15:00
An intuitionistic ALC description default logic
Alexandre Rademaker, Hermann Hauesler
15:00-15:30
An infinitary deduction system for CTL*
Luca Viganò, Marco Volpe, Margherita Zorzi
15:30-16:00
Modal functions as moody truth-functions
Pedro Falcão
14:30-15:00
Similarity-based Relaxed Instance Queries in EL++
Andreas Ecke
15:00-15:30
Resolution and Clause Learning for Multi-Valued CNF Formulas
David Mitchell
15:30-16:00
Many-valued Horn Logic is Hard
Stefan Borgwardt, Marco Cerami, Rafael Peñaloza
14:45-15:10
Query Answering in Resource-Based Answer Set Semantics
Stefania Costantini, Andrea Formisano
15:10-15:35
Declarative Encodings of Acyclicity Properties
Martin Gebser, Tomi Janhunen, Jussi Rintanen
15:35-16:00
Computing Secure Sets in Graphs using Answer Set Programming
M. Abseher, B. Bliem, G. Charwat, F. Dusberger, S. Woltran
14:45-16:00
Synthesis using EF-SMT Solvers (Invited Talk)
Ashish Tiwari
15:30-16:00 Discussion
16:30-17:00
Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
Jorge Baier, Brent Mombourquette, Sheila McIlraith
17:00-17:30
A Formalization of Programs in First-Order Logic with a Discrete Linear Order
Fangzhen Lin
17:30-18:00
Satisfiability of Alternating-time Temporal Epistemic Logic through Tableaux
Francesco Belardinelli
16:30-17:00
Linear Programs for Measuring Inconsistency in Probabilistic Logics
Nico Potyka
17:00-17:30
Reasoning with Uncertain Inputs in Possibilistic Networks
Salem Benferhat, Karim Tabia
17:30-18:00
Relational Logistic Regression
S.M. Kazemi, D. Buchman, K. Kersting, S. Natarajan, D. Poole
16:30-16:55
``Are Preferences Giving You a Headache?'' - ``Take asprin!''
Gerhard Brewka, James Delgrande, Javier Romero, Torsten Schaub
16:55-17:20
On the Implementation of Weak Constraints in WASP
Mario Alviano, Carmine Dodaro, Joao Marques-Silva, Francesco Ricca
17:20-17:45
Interactive Query-based Debugging of ASP Programs
Kostyantyn Shchekotykhin
17:45-18:10
Computing Answer Sets for Monadic Logic Programs via MapReduce
Ilias Tachmazidis, Grigoris Antoniou, Wolfgang Faber
16:30-17:15
Model Checking Hybrid Systems
Edmund M. Clarke
17:15-17:45
Towards a General Model of Evolving Interaction
Nachum Dershowitz
17:45-18:15
Compositional Temporal Synthesis
Moshe Vardi
16:30-17:15
The 1st Syntax-Guided Synthesis Competition (SyGuS)
Rajeev Alur
17:15-18:00
The 1st Synthesis Competition for Reactive Systems (SyntComp)
Swen Jacobs
16:30-17:00
SAT solving experiments in Vampire
Armin Biere, Ioan Dragan, Laura Kovacs, Andrei Voronkov
17:00-17:30
First Class Boolean Type in First-Order Theorem Proving and TPTP
Evgeny Kotelnikov, Laura Kovacs, Andrei Voronkov
17:30-18:00
Reasoning in First-Order Theories with Extensionality
Ashutosh Gupta, Laura Kovacs, Bernhard Kragl, Andrei Voronkov
16:30-17:00
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic
Hans De Nivelle
17:00-17:30
Computer-oriented inference search in first-order sequent logics
Alexander Lyaletski
17:30-18:00
Open Discussion
Workshop Organizers
16:30-17:00
A Graphical Notation for Probabilistic Specifications
Sebastian Nielebock, Tim Gonschorek, Frank Ortmeier
17:00-17:30
Assurance of some system reliability characteristics in formal design verification
Sergey Frenkel
16:30-17:00
Towards Evaluating the Usability of Interactive Theorem Provers
Sarah Grebing, Bernhard Beckert, Florian Böhl
17:00-17:30
Combined Reasoning with Sets and Aggregation Functions
Markus Bender
17:30-18:00
Tableau Development for a Bi-Intuitionistic Tense Logic
John Stell, Renate A. Schmidt, David Rydeheard
16:30-17:00
Towards Evaluating the Usability of Interactive Theorem Provers
Sarah Grebing, Bernhard Beckert, Florian Böhl
17:00-17:30
Combined Reasoning with Sets and Aggregation Functions
Markus Bender
17:30-18:00
Tableau Development for a Bi-Intuitionistic Tense Logic
John Stell, Renate A. Schmidt, David Rydeheard
16:30-17:00
Beagle as a HOL4 external ATP method
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish
17:00-17:30
Razor: Provenance and Exploration in Model-Finding
Salman Saghafi, Daniel Dougherty
17:30-18:00
SGGS Theorem Proving: an Exposition
Maria Paola Bonacina, David Plaisted
16:30-17:00
A Logic-based Framework for Verifying Consensus Algorithms
Cezara Dragoi, Thomas Henzinger, Helmut Veith, Josef Widder, Damien Zufferey
17:00-17:30
Monotonic Abstraction Techniques: from Parametric to Software Model Checking
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
17:30-18:00
Model Checking Distributed Consensus Algorithms
Giorgio Delzanno, Michele Tatarek
18:00-18:30
Model-Checking of Parameterized Timed-Systems
Luca Spalazzi, Francesco Spegni
16:30-17:00
On subexponentials, focusing and modalities in concurrent systems
Vivek Nigam, Carlos Olarte, Elaine Pimentel
17:00-17:30
Quantum state transformations and distributed temporal logic
Luca Viganò, Marco Volpe, Margherita Zorzi
17:30-18:00
Combining non-determinism and context awareness in consistency restoration systems
Ofer Arieli, Kostas Stefanidis, Anna Zamansky
16:30-17:00
Learning Preferences for Collaboration
Eva Armengol
17:00-17:30
Computing k-Rank Answers with Ontological CP-Nets
T. Di Noia, T. Lukasiewicz, M.V. Martinez, G. Simari, O. Tifrea-Marciuska
17:30-18:00
Multi-Attribute Decision Making using Weighted Description Logics
Erman Acar, Christian Meilicke
17:30-18:00 Discussion and Closing
18:00-19:00 Business Meeting
18:10-18:20 Closing
18:30-19:45
Situation Calculus: The Last 15 Years
Sheila McIlraith
19:45-20:00 KR Awards
10:15-10:45 Coffee Break
13:00-14:30 Lunch Break
16:00-16:30 Coffee Break
Disclaimer | Powered by EasyChair Smart Program