HCVS 2021: Horn Clauses for Verification and Synthesis Virtual Luxembourg, March 28, 2021 |
Conference website | https://www.sci.unich.it/hcvs21/ |
Submission link | https://easychair.org/conferences/?conf=hcvs2021 |
Submission deadline | February 19, 2021 |
Horn Clauses for Verification and Synthesis (HCVS)
Many Program Verification and Synthesis problems of interest can be modelled directly using Horn clauses and many recent advances in the CLP and CAV communities have centred around efficiently solving problems presented as Horn clauses.
This series of workshops aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.
Horn clauses for verification and synthesis have been advocated by these communities at different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
The workshop follows seven previous meetings: HCVS 2020 in Dublin, Ireland (ETAPS 2020), HCVS 2019 in Prague, Czech Republic (ETAPS 2019), HCVS 2018 in Oxford, UK (CAV, ICLP and IJCAR at FLoC 2018), HCVS 2017 in Gothenburg, Sweden (CADE), HCVS 2016 in Eindhoven, The Netherlands (ETAPS), HCVS 2015 in San Francisco, CA, USA (CAV), and HCVS 2014 in Vienna, Austria (VSL).
Submission Guidelines
- Regular papers (up to 12 pages plus bibliography in EPTCS format), which should present previously unpublished work (completed or in progress), including descriptions of research, tools, and applications.
- Tool papers (up to 4 pages in EPTCS format), including the papers written by the CHC-COMP participants, which can outline the theoretical framework, the architecture, the usage, and experiments of the tool.
- Extended abstracts (up to 3 pages in EPTCS format), which describe work in progress or aim to initiate discussions.
- Presentation-only papers, i.e., papers already submitted or presented at a conference or another workshop. Such papers can be submitted in any format, and will not be included in the workshop post-proceedings.
- Posters that are of interest to the workshop
List of Topics
- Analysis and verification of programs and systems of various kinds (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent, transition systems, Petri-nets, smart contracts)
- Program synthesis
- Program testing
- Program transformation
- Constraint solving
- Type systems
- Machine learning and automated reasoning
- CHC encoding of analysis and verification problems
- Resource analysis
- Case studies and tools
- Challenging problems
Committees
Program Committee
- Bishoksan Kafle, IMDEA Software Institute, Madrid, Spain (co-chair)
- Hossein Hojjat, Rochester Institute of Technology, NY, USA (co-chair)
- Gopal Gupta, University of Texas at Dallas, USA
- John Gallagher, Roskilde University, Denmark
- Philipp Ruemmer, Uppsala University, Sweden
- Andrey Rybalchenko, Microsoft Research, Cambridge, UK
- Pedro Lopez-Garcia, CSIC and IMDEA Software Institute, Madrid, Spain
- Emanuele De Angelis, IASI-CNR, Italy
- Fabio Fioravanti, University of Chieti-Pescara, Italy
- Daniel Neider, Max Planck Institute for Software Systems, Germany
- Arie Gurfinkel, University of Waterloo, Canada
- Ranjit Jhala, University of California San Diego, USA
- Martin Schäf, SRI International, USA
- He Zhu, Rutgers University, New Brunswick, USA
- Steven Ramsay, University of Bristol, UK
- Grigory Fedyukovich, Florida State University, USA
- Gidon Ernst, Ludwig Maximilian University of Munich, Germany
- David Monniaux, CNRS, VERIMAG, France
- Jorge A. Navas, SRI International, USA
Invited Speakers
- TBA
Publication
HCVS 2021 proceedings will be published electronically as a volume in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see http://www.eptcs.org/
Venue
The conference will be held in Virtually due to COVID-19.