VSL 2014: VIENNA SUMMER OF LOGIC 2014
VSL FOREWORD
VSL
PROGRAM
VOLUMES
VSL
|
FLoC
|
CAV
|
CSF
|
CSL-LICS
|
ICLP
|
IJCAR
|
ITP
|
RTA-TLCA
|
SAT
|
LC
|
LATD
|
KR
|
DL
|
NMR
|
2FC
|
ACL2
|
ADDCT
|
AISS
|
APPA
|
ARQNL
|
ARW-DT
|
ASA
|
ASPOCP
|
Automatheo
|
CHR
|
CICLOPS-WLPE
|
CLC
|
Coq
|
CSPSAT
|
DCM
|
DTP
|
EC2
|
FCS-FCC
|
FRIDA
|
FWFM
|
GeTFun
|
GSB
|
HCVS
|
HOL
|
HOPA
|
HOR
|
HSB
|
IFIP-WG16
|
INFINITY
|
iPRA
|
ITRS
|
IWC
|
Isabelle
|
KInAR
|
KR4HC
|
LaSh
|
LCC
|
LFMTP
|
LG
|
Linearity
|
LOLA
|
LSB
|
NCPROOFS
|
NLCS
|
NLSR
|
NSV
|
ORE
|
PAAR
|
ParSearchOpt
|
PAS
|
PC
|
PCCR
|
PLP
|
POS
|
PRUV
|
PSC
|
QBF
|
QED
|
QUANTIFY
|
RCRA
|
REORDER
|
RS
|
SMT
|
SD
|
SSV
|
STAST
|
SYNT
|
TermGraph
|
UITP
|
UNIF
|
Vampire
|
VEMDP
|
VERIFY
|
VeriSure
|
VPT
|
VSTTE
|
WING
|
WIR
|
WPTE
|
WST
|
WWV
PROGRAM FOR TUESDAY, JULY 22ND: TALK VIEW
Days:
previous day
next day
all days
View:
with abstracts
session overview
CAV
CSF
FLoC
VSL
GeTFun
IJCAR
ICLP
KR
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
20:30
21:00
21:30
10:45-11:15
Exact Learning of Lightweight Description Logic Ontologies
Boris Konev, Carsten Lutz, Ana Ozaki Rivera Castillo, Frank Wolter
11:15-11:45
Finite Model Reasoning in Horn Description Logics
Yazmin Ibanez-Garcia, Carsten Lutz, Thomas Schneider
11:45-12:15
Lightweight Description Logics and Branching Time: a Troublesome Marriage
Víctor Gutiérrez Basulto, Jean Christoph Jung, Thomas Schneider
10:45-11:15
Belief Change and Base Dependence
Mehrdad Oveisi, James P. Delgrande, Francis Jeffry Pelletier, Fred Popowich
11:15-11:45
Justified Beliefs by Justified Arguments
Davide Grossi, Wiebe Van Der Hoek
11:45-12:15
Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional
Andreas Herzig
10:45-11:05
Monadic Decomposition
Margus Veanes, Nikolaj Bjorner, Lev Nachmanson, Sergey Bereg
11:05-11:25
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters
11:25-11:45
Bit-Vector Rewriting with Automatic Rule Generation
Alexander Nadel
11:45-12:05
A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal
12:05-12:25
AVATAR: The New Architecture for First-Order Theorem Provers
Andrei Voronkov
12:25-12:45
Automating Separation Logic with Trees and Data
Ruzica Piskac, Thomas Wies, Damien Zufferey
12:45-12:55
A Nonlinear Real Arithmetic Fragment
Ashish Tiwari, Patrick Lincoln
12:55-13:05
Yices 2.2
Bruno Dutertre
10:45-11:05
Monadic Decomposition
Margus Veanes, Nikolaj Bjorner, Lev Nachmanson, Sergey Bereg
11:05-11:25
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters
11:25-11:45
Bit-Vector Rewriting with Automatic Rule Generation
Alexander Nadel
11:45-12:05
A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal
12:05-12:25
AVATAR: The New Architecture for First-Order Theorem Provers
Andrei Voronkov
12:25-12:45
Automating Separation Logic with Trees and Data
Ruzica Piskac, Thomas Wies, Damien Zufferey
12:45-12:55
A Nonlinear Real Arithmetic Fragment
Ashish Tiwari, Patrick Lincoln
12:55-13:05
Yices 2.2
Bruno Dutertre
10:45-11:30
Test of Time Awards: 20 Years - CLP(Intervals) Revisited
Pascal Van Hentenryck
11:30-12:00
SUNNY: a Lazy Portfolio Approach for Constraint Solving
Roberto Amadini, Maurizio Gabbrielli, Jacopo Mauro
12:00-12:30
Using Tabled Logic Programming to Solve the Petrobras Planning Problem
Roman Bartak, Neng-Fa Zhou
12:30-13:00
A Proof Theoretic Study of Soft Concurrent Constraint Programming
Vivek Nigam, Carlos Olarte, Elaine Pimentel
10:45-11:45
Structured Search and Learning
Kenneth McMillan
11:45-12:15
The Complexity of Theorem Proving in Circumscription and Minimal Entailment
Olaf Beyersdorff, Leroy Chew
12:15-12:45
Visibly Linear Temporal Logic
Laura Bozzelli, Cesar Sanchez
10:45-11:15
The Complexity of Estimating Systematic Risk in Networks
Benjamin Johnson, Aron Laszka, Jens Grossklags
11:15-11:45
Automated Generation of Attack Trees
Roberto Vigo, Flemming Nielson, Hanne Riis Nielson
11:45-12:15
Mignis: A semantic based tool for firewall configuration
P. Adão, C. Bozzato, G.-L. Dei Rossi, R. Focardi, F. Luccio
12:15-12:45
Provably Sound Browser-Based Enforcement of Web Session Integrity
M. Bugliesi, S. Calzavara, R. Focardi, W. Khan, M. Tempesta
10:45-11:30
Semi-implication and matrices
Arnon Avron
11:30-12:00
Yoneda’s embedding and Post-completeness
Hugo Macedo, Hermann Hauesler
12:00-12:30
On the characterization of broadly truth-functional logics
Sérgio Marcelino, Carlos Caleiro, João Marcos
12:30-13:00
On non-deterministic fuzzy negations
Hélida Santos, Benjamín Bedregal, Regivan Santiago, João Marcos
12:15-12:20
On Redundant Topological Constraints (Extended Abstract)
Matt Duckham, Sanjiang Li, Weiming Liu, Zhiguo Long
12:20-12:25
Knowledge Maps of Web Graphs
Valeria Fionda, Claudio Gutierrez, Giuseppe Pirró
12:25-12:30
On the Progression of Knowledge in Multiagent Systems
Vaishak Belle, Gerhard Lakemeyer
12:30-12:35
Heuristic Guided Optimization for Propositional Planning
Andreas Sideris, Yannis Dimopoulos
12:35-12:40
Action Theories over Generalized Databases with Equality Constraints (Extended Abstract)
Fabio Patrizi, Stavros Vassos
12:40-12:45
Representing and Reasoning About Time Travel Narratives: Foundational Concepts
Leora Morgenstern
12:45-12:50
Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas
Yuping Shen, Xishun Zhao
12:50-12:55
Using Answer Set Programming for Solving Boolean Games
Sofie De Clercq, Kim Bauters, Steven Schockaert, Martine De Cock, Ann Nowé
12:55-13:00
ASP Encodings of Acyclicity Properties
Martin Gebser, Tomi Janhunen, Jussi Rintanen
13:00-13:05
Stable Models of Multi-Valued Formulas: Partial vs. Total Functions
Michael Bartholomew, Joohyung Lee
12:15-12:20
First-Order Default Logic Revisited
Yi Zhou
12:20-12:25
Strong Equivalence of Non-monotonic Temporal Theories
Pedro Cabalar, Martín Diéguez
12:25-12:30
Belief Revision in the Propositional Closure of a Qualitative Algebra
Valmi Dufour-Lussier, Alice Hermann, Florence Le Ber, Jean Lieber
12:30-12:35
Minimal Change in AGM Revision for Non-classical Logics
Márcio Ribeiro, Renata Wassermann
12:35-12:40
Toward a Knowledge Level Analysis of Forgetting
James Delgrande
12:40-12:45
An Abductive Reasoning Approach to the Belief-Bias Effect
Luis Moniz Pereira, Emmanuelle-Anna Dietz, Steffen Hölldobler
12:45-12:50
Tracking Beliefs and Intentions in the Werewolf Game
Codruta Girlea, Eyal Amir, Roxana Girju
12:50-12:55
Axioms .2 and .4 as Interaction Axioms
Guillaume Aucher
12:55-13:00
Aggregative Deontic Detachment for Normative Reasoning
Xavier Parent, Leon van der Torre
14:30-15:00
Decidable Reasoning in a Fragment of the Epistemic Situation Calculus
Gerhard Lakemeyer, Hector J. Levesque
15:00-15:30
Model Checking Unbounded Artifact-Centric Systems
Alessio Lomuscio, Jakub Michaliszyn
15:30-16:00
State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
Babak Bagheri Hariri, Diego Calvanese, Alin Deutsch, Marco Montali
14:30-15:00
Skolemization for Weighted First-Order Model Counting
Guy Van den Broeck, Wannes Meert, Adnan Darwiche
15:00-15:30
Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint
Hannes Strass, Johannes Peter Wallner
15:30-16:00
The Parameterized Complexity of Reasoning Problems Beyond NP
Ronald De Haan, Stefan Szeider
14:30-14:50
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
14:50-15:10
Symbolic Resource Bound Inference for Functional Programs
Ravichandhran Madhavan, Viktor Kuncak
15:10-15:30
Proving Non-termination Using Max-SMT
D. Larraz, K. Nimkar, A. Oliveras, E. Rodríguez-Carbonell, A. Rubio
15:30-15:50
Termination Analysis by Learning Terminating Programs
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
15:50-16:10
Causal Termination of Multi-threaded Programs
Andrey Kupriyanov, Bernd Finkbeiner
14:30-15:30
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
Andrey Rybalchenko
15:30-16:00
Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
Alejandro Serrano, Pedro Lopez-Garcia, Manuel V. Hermenegildo
14:30-15:00
Count and Forget: Uniform Interpolation of SHQ-Ontologies
Patrick Koopmann, Renate A. Schmidt
15:00-15:30
Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation
Andreas Steigmiller, Birte Glimm, Thorsten Liebig
15:30-16:00
EL-ifying Ontologies
David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler, Ian Horrocks
14:30-15:30
Privacy in the Age of Augmented Reality
Alessandro Acquisti
14:30-15:00
Non truth-functional bivalent logics extending classical bivalent logics
Jean-Yves Béziau
15:00-15:30
A survey on Suszko’s Thesis and its formal developments
Sanderson Molick, João Marcos
15:30-16:00
Effective first-order reasoning about incomplete and inconsistent information
Arnon Avron, Beata Konikowska, Anna Zamansky
15:30-16:00
Balancing Societal Security and Individual Privacy: Accountable Escrow System
Jia Liu, Mark Ryan, Liqun Chen
16:30-17:00
Dynamic Consistency Checking in Goal-Directed Answer Set Programming
Kyle Marple, Gopal Gupta
17:00-17:30
Anytime Computation of Cautious Consequences in Answer Set Programming
Mario Alviano, Carmine Dodaro, Francesco Ricca
17:30-18:00
Efficient Computation of the Well-Founded Semantics over Big Data
Ilias Tachmazidis, Grigoris Antoniou, Wolfgang Faber
16:30-17:00
The Bayesian Description Logic BEL
İsmail İlkan Ceylan, Rafael Peñaloza
17:00-17:30
Otter proofs of theorems in Tarskian geometry
Michael Beeson, Larry Wos
17:30-17:50
NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
Nicola Olivetti, Gian Luca Pozzato
17:50-18:10
Knowledge Engineering for Large Ontologies with Sigma KEE 3.0
Adam Pease, Stephan Schulz
16:30-17:00
TUC: Time-sensitive and Modular Analysis of Anonymous Communication
Michael Backes, Praveen Manoharan, Esfandiar Mohammadi
17:00-17:30
Differential Privacy: An Economic Method for Choosing Epsilon
J. Hsu, M. Gaboardi, A. Haeberlen, S. Khanna, A. Narayan, B. Pierce, A. Roth
17:30-18:00
Proving differential privacy in Hoare logic
G. Barthe, M. Gaboardi, E.J. Gallego Arias, J. Hsu, C. Kunz, P.-Y. Strub
18:00-18:30
Surveillance and Privacy
Jonathan Mayer
16:30-17:00
DC Minute Madness
16:30-17:15
Separating truth and proof in the Logic of Proofs
Roman Kuznets
16:40-17:00
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher
17:00-17:20
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath
Suho Lee, Karem A. Sakallah
17:20-17:30
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan
17:00-18:30
Poster Session
17:30-18:30
Business Meeting
18:00-19:00
SIGLOG Meeting
19:30-21:30
KR Banquet
08:45-09:45
VSL Keynote Talk: Verification of Computer Systems with Model Checking
Edmund Clarke
10:15-10:45
Coffee Break
13:00-14:30
Lunch Break
16:00-16:30
Coffee Break
Disclaimer
|
Powered by EasyChair Smart Program