 |
See all Events
92 elements available | |
CALL FOR PARTICIPATION
PCCR 2010
Parameterized Complexity of Computational Reasoning
Satellite Workshop of MFCS & CSL
Brno, Czech Republic, 28 August 2010
http://www.kr.tuwien.ac.at/drm/pccr2010
This workshop aims to support a fruitful exchange of ideas between the
research on parameterized complexity on one side and the research on various
forms of computational reasoning (such as nonmonotonic, probabilistic, and
constraint-based reasoning) on the other. The workshop features invited
and contributed talks and presentations of surveys and new technical results.
Invited speakers are:
* Mike Fellows, Charles Darwin University
* Nicola Galesi, Sapienza University of Rome
* Gregory Gutin, University of London
* Petr Hlineny, Masaryk University Brno
* Reinhard Pichler, Vienna University of Technology
List of Presentations:
* Mike Fellows: An Overview of Parameterized Complexity and Recent Research
Directions in Constraint Satisfaction and Artificial Intelligence
* Gregory Gutin, Keynote Talk: Complexity of Permutation Constraint Satisfaction
Problems Parameterized Above Average
* Petr Hlineny: Where Myhill-Nerode Theorem meets Parameterized Algorithmics
* Reinhard Pichler: Bounded Treewidth in Non-Monotonic Reasoning
* M. Praveen: Does Treewidth Help in Modal Satisfiability?
* Fran Rosamond: On the Complexity of Some Constraint Satisfaction Problems with
Global Constraints and Convexity
* Nicola Galesi: The Complexity of Proofs in Parameterized Resolution
* Yijia Chen: Optimal Proof Systems, Slicewise Monotone Parameterized Problems,
and Logics for PTIME
For the schedule of the talks, see http://www.kr.tuwien.ac.at/drm/pccr2010/
For information on how to register and local information please consult the
MFCS-CSL 2010 web-site http://mfcsl2010.fi.muni.cz/
The workshop is organized by Igor Razgon, Marko Samer, Stefan Szeider (chair),
and Stefan Woltran.
|
| |  | |  |
| | |
| | | Call for papers for CROCS at CP-10, the 3rd International Workshop on Constraint Reasoning and Optimization for Computational Sustainability, to be held on September 6, 2010 in St Andrews, Scotland, in conjunction with the CP-10 conference.
For submission and other details, please see http://www.computational-sustainability.org/crocs-at-cp10 |
| | | | |
| | |
| |
JELIA 2010 CALL FOR PARTICIPATION
=================================
12th European Conference on Logics in Artificial Intelligence
Helsinki, Finland, September 13-15, 2010
http://jelia2010.tkk.fi/
Logics provide a formal basis and key descriptive notation for the study
and development of applications and systems in Artificial Intelligence
(AI). With the depth and maturity of formalisms, methodologies, and
systems today, such logics are increasingly important. The European
Conference on Logics in Artificial Intelligence (or Journées Européennes
sur la Logique en Intelligence Artificielle --- JELIA) began back in
1988, as a workshop, in response to the need for a European forum for
the discussion of emerging work in this field. Since then, JELIA has
been organized biennially, with English as the official language, and
with proceedings published in Springer-Verlag's Lecture Notes in
Artificial Intelligence series. In 2010 the conference is organized for
the first time in Scandinavia, following previous meetings mainly taking
place in Central and Southern Europe (see the general website
http://www.jelia.eu/ for details). The increasing interest in this
forum, its international level with growing participation from
researchers outside Europe, and the overall technical quality, has
turned JELIA into a major biennial forum for the discussion of
logic-based approaches to AI.
Registration and Travel Information
===================================
Registration as well as travel and accommodation information is
available on JELIA 2010 web pages http://jelia2010.tkk.fi/
JELIA 2010 Registration Fees
Early (until Aug 9) Late (Aug 10 - Sep 1)
Regular 250 EUR 400 EUR
Student 150 EUR 250 EUR
including JELIA 2010 technical sessions and invited talks, coffee
breaks, the combined JELIA/PGM welcome reception on September 13,
conference Banquet and excursion on September 14, JELIA 2010 LNAI
conference proceedings, and conference accessories (bag, programme,
info, ...)
Scientific Program
==================
The scientific program consists of three invited talks, 26 regular
papers, and 5 system descriptions. See details in the preliminary
program at http://jelia2010.tkk.fi/schedule.shtml
Invited Speakers
================
Gerhard Brewka (http://www.informatik.uni-leipzig.de/~brewka/):
Nonmonotonic Tools for Argumentation
Adnan Darwiche (http://www.cs.ucla.edu/~darwiche/):
Relax, Compensate and then Recover:
A Theory of Anytime, Approximate Inference
Stéphane Demri (http://www.lsv.ens-cachan.fr/~demri/):
Counter Systems for Data Logics
Venue
=====
The conference will be held in the main building of University of
Helsinki, located in the center of Helsinki. Founded in 1550, Helsinki
has been the Finnish capital since 1812, when it was rebuilt in the
Empire style by the orders of the Czar of Russia, hence sharing
architectural similarities with St. Petersburg even today. Located on
the Baltic peninsula centrally between the east and the west, Helsinki
"the Daughter of the Baltic" is a city full of contrasts: light and
white in summer while dark but full of warmth in winter, with a
combination of high-tech, contemporary design, and ever-present nature.
Finnish design has made Helsinki world famous, and recently Helsinki
was appointed World Design Capital 2012.
Co-located events
=================
European Workshop on Probabilistic Graphical Models (PGM)
http://www.helsinki.fi/pgm2010/
|
| | | | |
| | |
| |
---------------------------------------------------------------------
SAT 2010 - 13th International Conference on
Theory and Applications of Satisfiability Testing
Edinburgh, UK, July 11-14, 2010
http://ie.technion.ac.il/SAT10/
as part of FLoC 2010 - Federated Logic Conference
http://www.floc-conference.org/
Call for Participation
---------------------------------------------------------------------
SAT is the primary annual meeting for researchers studying the
propositional satisfiability problem. The technical programme will
consist of presentations of high-quality original research papers, a
tutorial presentation, several invited talks, and presentations of
solver competition results.
Registration, accommodation, and travel/visa information for all FLoC
conferences and workshops is on the FLoC 2010 web pages.
DEADLINES:
Early registration deadline: 17 May 2010
Standard registration: 18 May 2010 - 30 June 2010
Late registration: after 30 June 2010
TECHNICAL PROGRAMME
Presentation of 2 invited SAT talks
Presentation of 4 plenary/keynote FLoC invited talks
Presentation of 35 technical research papers
Presentation of 3 solver competitions
SAT INVITED SPEAKERS
Yehuda Naveh, IBM Haifa Research Lab, Israel
Ramamohan Paturi, University of California, USA
FLoC PLENARY AND KEYNOTE SPEAKERS
David Harel, Weizmann Institute of Science, Israel
Gordon Plotkin, University of Edinburgh, UK
Georg Gottlob, University of Oxford, UK
J Strother Moore, University of Texas, USA
SAT INVITED TUTORIAL SPEAKER
Daniel Kroening, University of Oxford, UK
SAT AFFILIATED COMPETITIONS
MAX-SAT Evaluation 2010
Pseudo-Boolean Competition 2010
SAT-Race 2010
SAT AFFILIATED WORKSHOPS
PPC 2010 - Propositional Proof Complexity (July 9)
POS 2010 - Pragmatics of SAT (July 10)
LoCoCo 2010 - Logics for Component Configuration (July 10)
SMT 2010 - Satisfiability Modulo Theories (with CAV, July 14-15)
LaSh 2010 - Logic and Search (with ICLP, July 15)
SOCIAL EVENTS
Drinks Reception - July 11 at Edinburgh Castle
Conference Banquet - July 13 at "Our Dynamic Earth"
PROCEEDINGS
At registration the proceedings of all FLoC conferences and workshops
will be provided, at no additional cost, on a USB stick. Hard copy SAT
2010 proceedings are optionally available, for an additional
cost. Remember to tick the hard copy proceedings box when you register.
Please note that hard copies are offered at approximately 50% discount
during registration and will possibly not be on sale later on or during
the conference.
REGISTRATION
For on line registration for SAT, please follow the link on the FLoC
website at http://floc-conference.org/registration.html
ACCOMMODATION
Very affordable accommodation can be booked via the FloC registration,
see http://floc-conference.org/accommodation.html
|
| | | | |
| | |
| | | CALL FOR PARTICIPATION (feel free to distribute; apologies for multiple copies)
A Workshop on Tractability will take place on July 5-6, 2010 at Microsoft Research, Cambridge, UK.
(visiting us is easy!)
This workshop will bring together distinguished researchers to discuss their viewpoints on the question: What makes some difficult (e.g. NP-hard) problems tractable in practice? It will provide a place for interactions between experts on a variety of approaches to this question, including both theoreticians and practitioners.
The workshop consists of an exciting set of invited talks, and will leave ample space for discussions.
Participation is free of charge and interested students and researchers are welcome to attend. Registration is necessary: please write to "msrcevnt" followed by “at microsoft” and ending with “dot com” to inform us that you wish to attend. Please indicate your:
- Full name
- Company or University
- Country of residence
- Email address
|
| | | | |
| | |
| | 12th European Conference on Logics in Artificial Intelligence
Helsinki, Finland, September 13-15, 2010
http://jelia2010.tkk.fi/
The aim of JELIA 2010 is to bring together active researchers interested in all aspects concerning the use of logics in Artificial Intelligence to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross-fertilisation of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in Artificial Intelligence including:
- Abductive and inductive reasoning
- Answer set programming
- Applications and foundations of logic-based AI systems
- Argumentation systems
- Automated reasoning including satisfiability checking and its extensions
- Computational complexity and expressiveness
- Description logics and other logical approaches to semantic web and ontologies
- Hybrid reasoning systems
- Knowledge representation, reasoning, and compilation
- Logic programming and constraint programming
- Logics for uncertain and probabilistic reasoning
- Logics in machine learning
- Logics in multi-agent systems, games, and social choice
- Non-classical such as modal, temporal, spatial, paraconsistent, and hybrid logics
- Nonmonotonic reasoning, belief revision, and updates
- Planning and diagnosis based on logic
- Preferences
- Reasoning about actions and causality
Important Dates
- Deadline for abstract submission: May 3, 2010
- Deadline for paper submission: May 7, 2010
- Notification of acceptance: June 11, 2010
- Camera Ready Copy: June 30, 2010
Paper Submission
Proceedings will be published by Springer-Verlag in the Lecture Notes on Artificial Intelligence series. Papers should be written in English, and should be formatted according to the standard Springer LNCS style. All submissions must be received by 23:59 GMT on May 3, 2010 (abstract) and May 7, 2010 (full paper), and should be electronically submitted via the link available on the JELIA 2010 web page. There are two categories for submissions:
- A. Regular papers Submissions should not exceed 13 pages including figures, references, etc., and should contain original research, and sufficient detail to assess the merits and relevance of the contribution. Submissions must not have been previously published or be simultaneously submitted for publication elsewhere.
- B. System descriptions Submissions should not exceed 4 pages, and should describe an implemented system and its application area(s). A demonstration is expected to accompany a system presentation. Papers describing systems that have already been presented in JELIA before will be accepted only if significant and clear enhancements to the system are reported and implemented.
|
| | | | |
| | |
| | Please join us for the Twelfth International Conference on the
Principles of Knowledge Representation and Reasoning (KR 2010), to be
held May 9-13, 2010 at The Sutton Place Hotel, in Toronto, Ontario,
Canada.
The deadline for registration is April 9th!
KR 2010 will be co-located with AAMAS, FOIS, ICAPS, and NMR. Options for cross-registration are
available. |
| | | | |
| | |
| | 12th European Conference on Logics in Artificial Intelligence
Helsinki, Finland, September 13-15, 2010
http://jelia2010.tkk.fi/
The aim of JELIA 2010 is to bring together active researchers interested in all aspects concerning the use of logics in Artificial Intelligence to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross-fertilisation of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in Artificial Intelligence including:
- Abductive and inductive reasoning
- Answer set programming
- Applications and foundations of logic-based AI systems
- Argumentation systems
- Automated reasoning including satisfiability checking and its extensions
- Computational complexity and expressiveness
- Description logics and other logical approaches to semantic web and ontologies
- Hybrid reasoning systems
- Knowledge representation, reasoning, and compilation
- Logic programming and constraint programming
- Logics for uncertain and probabilistic reasoning
- Logics in machine learning
- Logics in multi-agent systems, games, and social choice
- Non-classical such as modal, temporal, spatial, paraconsistent, and hybrid logics
- Nonmonotonic reasoning, belief revision, and updates
- Planning and diagnosis based on logic
- Preferences
- Reasoning about actions and causality
Important Dates
- Deadline for abstract submission: May 3, 2010
- Deadline for paper submission: May 7, 2010
- Notification of acceptance: June 11, 2010
- Camera Ready Copy: June 30, 2010
Paper Submission
Proceedings will be published by Springer-Verlag in the Lecture Notes on Artificial Intelligence series. Papers should be written in English, and should be formatted according to the standard Springer LNCS style. All submissions must be received by 23:59 GMT on May 3, 2010 (abstract) and May 7, 2010 (full paper), and should be electronically submitted via the link available on the JELIA 2010 web page. There are two categories for submissions:
- A. Regular papers Submissions should not exceed 13 pages including figures, references, etc., and should contain original research, and sufficient detail to assess the merits and relevance of the contribution. Submissions must not have been previously published or be simultaneously submitted for publication elsewhere.
- B. System descriptions Submissions should not exceed 4 pages, and should describe an implemented system and its application area(s). A demonstration is expected to accompany a system presentation. Papers describing systems that have already been presented in JELIA before will be accepted only if significant and clear enhancements to the system are reported and implemented.
|
| | | | |
| | |
| | | The purpose of the LaSh workshops (this is the third) is to bring together researchers interested in theory and practice of logic-based methods for solving combinatorial search and optimization problems. Work on solvers (SAT, SMT, MaxSAT, etc), as well as work on specification and modelling languages, grounding, problem representations and transformations, etc., is welcome. LaSh 2010 will be held as a joint SAT/ICLP workshop at FLoC 2010, on July 15 in Edinburgh. Paper submissions are due by April 7. |
| | | | |
| | |
| | The International Conference on Principles and Practice of Constraint Programming is the annual conference on all aspects of computing with constraints, including: theory, algorithms, applications, environments, languages, models and systems.
This year it will be held in St Andrews, Scotland from 6-10th September 2010.
Submission for tutorial and workshop proposals, as well as submission of technical and application papers is currently open. PhD students are invited to apply for the Doctoral Programme.
See the website for details. |
| | | | |
| | |
| |
Workshop of SAT at FLoC 2010, Edinburgh, Scotland, July 10, 2010
First Call for Papers
Scope:
======
Modern software distributions are based on the notion of components, which
denote units of independent development and deployment. Components provide
the necessary flexibility when organizing a complex software distribution,
but also are a challenge when it comes to selecting components from a large
repository of possible choices, and configuring these components according
to user needs, resource constraints, and interdependencies with other
components. Representing and solving configuration problems is a hot topic
of great importance for many application domains. Some well-known examples
of complex systems of components in the world of Free and Open Source
software are the different distributions for GNU/Linux, BSD, or Eclipse
plugins.
Understanding and solving these questions is an attractive research
topic since the problems to be solved are complex and interesting for
researchers working on solving techniques, and on the other hand have
the potential of high impact on the way the software we all use
everyday is developed and deployed. Not only adequate logical
formalisms to represent a configuration problem are required, but also
sophisticated reasoning technologies to deal with large amounts of
data. Further relevant aspects include diagnosis of failed
configuration settings and an intelligent behavior dealing with user
preferences.
This workshop will focus on logic-based methods for specifying and solving
complex configuration problems for software components. The goal of the
workshop is to bring together both researchers and practitioners active in
the area of component configuration of software systems, using different
modeling and solving techniques, such as constraint and logic programming,
description logics, satisfiability and its extensions. The workshop will be
an opportunity to discuss common and complementary solutions for solving
component configuration.
Invited Talk
============
An invited talk will be given by Carsten Sinz (University of Karlsruhe).
MISC 2010
=========
The first Mancoosi International Solver Competition will be held in
conjunction with the LoCoCo workshop.
Important Dates
===============
Friday, March 26 Submission deadline
Friday, April 23 Notification about acceptance
Friday, May 21 Final paper due
Saturday, July 10 Workshop
Submission and Publication
==========================
We welcome submissions of various types of presentations related to
the topics of the workshop, such as
- full research papers
- abstracts of ongoing work
- tutorial overview papers
- summaries of research projects
- system descriptions, if possible including system demonstration at the
workshop. These must provide the means to download and evaluate the
system, with preference to distribution under an open source licence.
Program Committee
=================
Daniel Le Berre (Universite d'Artois, France)
Roberto Di Cosmo (Universite Paris-Diderot, France)
Georg Gottlob (Oxford University, UK)
Pascal van Hentenryck (Brown University, USA)
Matti Jarvisalo (University of Helsinki, Finland)
Ines Lynce (INESC-ID, Lisbon, Portugal), co-chair
Toni Mancini (Sapienza Universita di Roma, Italy)
Albert Oliveras (Technical University of Catalonia, Barcelona, Spain)
Christian Schulte (KTH, Stockholm, Sweden)
Ralf Treinen (Universite Paris-Diderot, France), co-chair
Nic Wilson (UCC, Cork, Irland) |
| | | | |
| | |
| | JELIA 2010 CALL FOR PAPERS
12th European Conference on Logics in Artificial Intelligence
Helsinki, Finland, September 13-15, 2010
http://jelia2010.tkk.fi/
The aim of JELIA 2010 is to bring together active researchers interested in
all aspects concerning the use of logics in Artificial Intelligence
to discuss current research, results, problems, and applications of both
theoretical and practical nature. JELIA strives to foster links and
facilitate cross-fertilisation of ideas among researchers from
various disciplines, among researchers from academia and industry,
and between theoreticians and practitioners.
Authors are invited to submit papers presenting original and unpublished
research in all areas related to the use of logics in Artificial Intelligence
including:
- Abductive and inductive reasoning
- Answer set programming
- Applications and foundations of logic-based AI systems
- Argumentation systems
- Automated reasoning including satisfiability checking and its extensions
- Computational complexity and expressiveness
- Description logics and other logical approaches to
semantic web and ontologies
- Hybrid reasoning systems
- Knowledge representation, reasoning, and compilation
- Logic programming and constraint programming
- Logics for uncertain and probabilistic reasoning
- Logics in machine learning
- Logics in multi-agent systems, games, and social choice
- Non-classical such as modal, temporal, spatial,
paraconsistent, and hybrid logics
- Nonmonotonic reasoning, belief revision, and updates
- Planning and diagnosis based on logic
- Preferences
- Reasoning about actions and causality
Important Dates
- Deadline for abstract submission: May 3, 2010
- Deadline for paper submission: May 7, 2010
- Notification of acceptance: June 11, 2010
- Camera Ready Copy: June 30, 2010
Paper Submission
Proceedings will be published by Springer-Verlag in the Lecture Notes on
Artificial Intelligence series. Papers should be written in English,
and should be formatted according to the standard Springer LNCS style.
All submissions must be received by 23:59 GMT on May 3, 2010 (abstract)
and May 7, 2010 (full paper), and should be electronically submitted
via the link available on the JELIA 2010 web page.
There are two categories for submissions:
- A. Regular papers
Submissions should not exceed 13 pages including figures, references, etc.,
and should contain original research, and sufficient detail to assess
the merits and relevance of the contribution. Submissions must not have
been previously published or be simultaneously submitted for publication
elsewhere.
- B. System descriptions
Submissions should not exceed 4 pages, and should describe an implemented
system and its application area(s). A demonstration is expected to
accompany a system presentation. Papers describing systems that have
already been presented in JELIA before will be accepted only if significant
and clear enhancements to the system are reported and implemented.
|
| | | | |
| | |
| | |
| | Important dates
- The deadline for registration is October 15st (unchanged).
- The new deadline for solvers and formulas submission is October 31st (NEW).
Only registered participants can send their contribution. |
| | | | |
| | |
| | | Random QBFs track added at QBFEVAL'10. For all informations, please visit the QBFEVAL web portal (www.qbfeval.org). |
| | | | |
| | |
| | CROCS-09 submission deadline extended to August 23, 2009
Call for Papers, Abstracts, and Discussion Topics: CROCS 2009, the First International Workshop on Constraint Reasoning and Optimization for Computational Sustainability, September 20, 2009, Lisbon, Portugal
To be held in conjunction with CP-09, the 15th International Conference on Principles and Practice of Constraint Programming.
For more information on this workshop as well as the newly emerging interdisciplinary field of computational sustainability, please visit http://www.computational-sustainability.org/crocs09.
Best,
Ashish |
| | | | |
| | |
| |
Call for Papers
Formal Methods and Verification Track
Design, Automation & Test in Europe
Dresden, Germany
March 8-12, 2010
The Design, Automation and Test in Europe conference and exhibition is the
premiere European event bringing together designers and design automation
users, researchers and vendors, as well as specialists in the hardware and
software design, test and manufacturing of electronic circuits and systems.
This five-day event consists of a conference with plenary keynotes, regular
papers, interactive presentations, panels and hot-topic sessions,
tutorials, master courses and workshops. DATE is also Europe's leading
commercial exhibition showing the state-of-the-art in design and test
tools, methodologies, IP and design services. Both the conference and the
exhibition, together with the many user group meetings, fringe meetings,
university booth and social events offer a wide variety of opportunities to
meet and exchange information.
The Formal Methods and Verification Track (D8) is devoted to the
presentation and discussion of state-of-the-art advances in a variety of
focus areas, including but not limited to:
* Formal verification and specification techniques including equivalence
checking, model checking, symbolic simulation, theorem-proving,
abstraction and refinement techniques, and real time verification
* Technologies supporting formal verification, including SMT, SAT, BDD,
ATPG, and related work
* Semi-formal verification techniques
* Applications and case studies, including formal verification of IPs,
SoCs, cores and real-time/embedded systems
* Verification in practice, namely the integration of verification into
the design flow
Jason Baumgartner (Chair) IBM Corporation, jason.r.baumgartner@gmail.com
Joao Marques-Silva (Co-Chair) University College Dublin, jpms@ucd.ie
Armin Biere Johannes Kepler University
Per Bjesse Synopsys Inc.
Roderick Bloem Graz University of Technology
Gianpiero Cabodi Politecnico di Torino
Alessandro Cimatti FBK-IRST
Daniel Kroening Oxford University
Wolfgang Kunz University of Kaiserslautern
Panagiotis Manolios Northeastern University
All manuscripts must be submitted electronically by September 6th, 2009,
following the instructions on the conference Web page:
www.date-conference.com
|
| | | | |
| | |
| | | Call for Papers, Abstracts, and Discussion Topics: CROCS 2009
First International Workshop on Constraint Reasoning and Optimization
for Computational Sustainability
September 20, 2009, Lisbon, Portugal
To be held in conjunction with CP-09, the 15th International
Conference on Principles and Practice of Constraint Programming.
For more information on this workshop as well as the newly emerging interdisciplinary field of computational sustainability, please visit http://www.computational-sustainability.org/crocs09.
Best,
Ashish |
| | | | |
| | |
| |
SymCon'09 First Call for Papers
The Ninth International Workshop on Symmetry and Constraint Satisfaction Problems
To be held at the Fifteenth International Conference on Principles and Practice of Constraint Programming (CP 2009)
Lisbon, Portugal, September 20, 2009
Submission deadline: Monday, 29 June 2009
Notification of acceptance: Friday, 31 July 2009
Camera ready deadline: Friday, 14 August 2009
Workshop: Sunday, 20th September 2009
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
Workshop topics include, but are not limited to:
- Symmetry definition: semantic symmetry, syntactic symmetry, constraint symmetry, solution symmetry
- Automatic symmetry detection: static approaches and dynamic approaches
- Global symmetry detection and elimination
- Dynamic symmetry detection and elimination
- Combining symmetry breaking techniques
- Exploiting weak forms of symmetries like "dominance" and "almost-symmetries"
- Case studies of problems that exhibit interesting symmetries
- Application of computational group theory techniques to symmetry breaking
- Heuristics that use information about symmetry to guide search - Elimination and avoidance of symmetry by re-modelling
- Dynamic avoidance of symmetric states during search
- Complexity analysis of symmetry breaking techniques
- Application of CSPs to symmetry and related algebraic problems - Comparing symmetry breaking techniques in constraint
programming with techniques for dealing with symmetry in other search domains
- Symmetry in CNF formulas and OBF formulas
- Symmetry in finite model search in first order logic
- Novel exploitation of symmetry in varied search domains of interest to the CP community
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
|
| | | | |
| | |
|  | |  | | | | | Date: | 11-May-2009 | | Title: | HLDVT 2009: Call for Papers
| | Hits: | 556 | | Contributed by: | Anonymous | | Keywords: | BDD, Random 3SAT, Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, SAT tools, call for papers, SAT-Based, SAT/CP, Hybrid solver, null, null, null, null, null |
| | | |  |  | |
| | | Call for Papers
***************************************************************
HLDVT 2009
IEEE International High-Level Design, Validation and Test Workshop
http://www.hldvt.com/09/
Grand Hyatt, San Francisco, California, November 4-6, 2009
***************************************************************
Please visit http://www.hldvt.com/09/HLDVT09_cfp.pdf |
| | | | |
| | |
| | | | | | | | Date: | 27-Apr-2009 | | Title: | The Second Answer Set Programming Competition
| | Hits: | 443 | | Contributed by: | | |
Last Call for Papers
Bit-Precise Reasoning 2009 (BPR'09)
Second International Workshop
June 26, Grenoble, France,
Affiliated to CAV'09
http://fmv.jku.at/bpr09
Important Dates
8. May Abstract Submission
15. May Paper Submission
22. May Author Notification
12. June Final Version
Chairs
Armin Biere, JKU, Austria
Priyank Kalla, Univ. of Utah, USA
Program Comittee
Nina Amla, Cadence, USA
Domagoj Babic, Consultant, USA
Clark Barrett, New York Univ., USA
Per Bjesse, Synopsys, USA
Jim Grundy, Intel, USA
Michael Hsiao, Virginia Tech, USA
Daniel Kröning, Univ. of Oxford, UK
Leonardo de Moura, Microsoft, USA
Karen Yorav, IBM, Israel
History
The first workshop on Bit-Precise Reasoning (BPR'08) took
place in Princeton in 2008 and was also affiliated to CAV.
Overview
Bit-precise reasoning (BPR) is a new and promising trend in
automated theorem proving. Traditionally, many theorem provers
approximate bit-vector arithmetic by unbounded integers
or even floating-point. Such approximations fail to model
the boundary behavior of bit-vector arithmetic (overflows
and underflows) accurately. In addition, reasoning about
non-linear operators over unbounded integers is particularly
problematic (undecidable). Recent advances in bit-vector
arithmetic decision procedures indicate that BPR could
become a practical method capable of handling both boundary
conditions and nonlinear operators precisely.
Scope
The primary goal of the BPR Workshop is to bring together both
researchers and users of BPR technology and provide them with
a forum for presenting and discussing not only new theoretical
ideas, but also implementation and evaluation techniques that,
due to either their premature state or their experimental
nature, are unlikely to be accepted for publication in larger
conferences.
Submission
We have two types of papers. Original papers, which will
also be part of the formal proceedings, should contain
original research and sufficient detail to asses the
merits of the submission. On the other hand, we also allow
presentation-only papers, that should describe work recently
published or submitted to some other event. We see this as
a way to provide additional access to important developments
that BPR attendees may be unaware of.
Submission can only be accepted in PDF and should be prepared
using LaTeX with LNCS format using standard margins and
fonts. There is a page limit of 12 pages. Please submit your
paper via EasyChair using the link provided at fmv.jku.at/bpr09.
|
| | | | |
| | |
| | | | | | | | Date: | 03-Mar-2009 | | Title: | Call for Participation: The Second Answer Set Programming Competition
| | Hits: | 499 | | Contributed by: | | | | | | | | | Date: | 04-Feb-2009 | | Title: | The Second Answer Set Programming Competition
| | Hits: | 547 | | Contributed by: | | |
The 2009 pseudo-Boolean competition is organized as a special event of the SAT 2009
conference. Like the previous evaluations (PB05, PB06, PB07), the goal is to assess
the state of the art in the field of pseudo-Boolean solvers.
The deadline for submitting benchmarks or solvers is fixed to April 13, 2009.
Other deadlines as well as the evaluation rules are available at
http://www.cril.univ-artois.fr/PB09/
We would particularly appreciate the submission of
- any kind of pseudo-Boolean solvers
- industrial benchmarks
- benchmarks generators
- benchmarks with a wide distribution of their number of clauses,
cardinality constraints and pseudo-Boolean constraints
- benchmarks with non-linear constraints
|
| | | | |
| | |
| | | Kelowna, BC, Canada May 24, 2009
CALL FOR PAPERS – Deadline January 30th, 2009
AI 2009, the twenty-second Canadian Conference on Artificial Intelligence, invites graduate students to submit four-page extended abstracts of their thesis for possible inclusion in the AI 2009 Graduate Student Symposium. The symposium will be a one-day pre-conference event, where students of accepted abstracts will be invited to give a presentation on their thesis work before a group of peers as well as a small team of expert AI researchers who would offer a critique of each presentation and provide support, advice, and mentoring.
Important Dates
Full paper submission due: January 30th, 2009
Notification of acceptance: March 3rd, 2009
Final paper due: March 16th, 2009
Graduate Student Symposium: May 24th, 2009
Contact
Svetlana.Kiritchenko at nrc-cnrc.gc.ca |
| | | | |
| | |
| |
Applied Formal Verification Track
EUROCAST'09
Las Palmas, Canary Islands, Spain
IMPORTANT DATES
February 15-20, 2009
Ext. Abstracts: 31. Oktober, 2008 (2 pages LNCS style)
Conference: 15.-20. February, 2009
Full Papers: 30. April, 2009 (prob. again in LNCS)
http://www.iuctc.ulpgc.es/spain/eurocast2009/index.html
TOPICS
In the last decade the topic of formal verification has left
the ivory tower of academic research. In hardware design many
industrial projects rely in one way or the other on formal
verification tools. The same trend can be seen in software.
The main driving force behind this development is on one hand
the increasing complexity of todays design, which can not
be handled by traditional testing techniques alone, and on
the other hand by the increasing dependability of our daily
lives on computer systems. However, also the core engines,
such as SAT solvers are becoming much more powerful.
In this workshop we want to bring to together researchers in
applied formal verification. We focus on formal verification
engines. The topics include, but are not limited to the
following
Satisfiability (SAT)
Satisfiability Modulo Theories (SMT)
Quantified Boolean Formulas (QBF)
Constraint Programming (CP)
Equivalence Checking (EC)
Model Checking (MC)
Theorem Proving (TP)
Beside papers on verification engines we also welcome case
studies and papers on the border line of verification, including
synthesis, compilation and modelling. Our main goal is to
improve practicability and scalability of formal methods.
SUBMISSION
An extended two pages abstract, including references in English
with indication of the workshop of the intended contribution,
e.g. 'Applied Formal Verification' must be sent (via webpage or
by e-mail) before October, 31, 2008 to the Organizing Commitee
Chairman: aquesada@dis.ulpgc.es.
|
| | | | |
| | |
| | | AI'09, the twenty-second Canadian Conference on Artificial Intelligence,
will be held in Kelowna, British Columbia (May 25-27, 2009). The
organizers invite papers that present original work in all areas of
Artificial Intelligence.
Paper submission due: January 23rd, 2009
Notification of acceptance: March 3rd, 2009
Final paper due: March 16th, 2009 |
| | | | |
| | |
| |
* ______________________________________________________________________ *
The RCRA group (Knowledge Representation & Automated Reasoning) of the
AI*IA (Italian Association for Artificial Intelligence)
http://www.dis.uniroma1.it/~rcra
organises the
15th RCRA workshop:
Experimental evaluation of algorithms for solving problems
with combinatorial explosion
http://www.dis.uniroma1.it/~rcra08
rcra08@dis.uniroma1.it
* ______________________________________________________________________ *
This workshop follows the series of the RCRA (Knowledge Representation
and Automated Reasoning) annual meeting, held since 1994. The success
of the previous events shows that RCRA is becoming a major forum for
exchanging ideas and proposing experimentation methodologies for
algorithms in artificial intelligence.
*** Workshop post-proceedings will be published in the Elsevier ***
*** Journal of Algorithms in Logic, Informatics and Cognition. ***
* ______________________________________________________________________ *
DATES
Two days in December 2008, co-located with ICLP 2008 (9-13 December 2008)
(exact dates to be announced)
VENUE
Udine, Italy
AIMS AND SCOPE
[see details on the full CFP]
WORKSHOP CHAIRS
* Marco Gavanelli, Università degli Studi di Ferrara, Italy
* Toni Mancini, Sapienza Università di Roma, Italy
SUBMISSIONS
Authors are invited to submit either original papers, or papers that appear on
conference proceedings.
At the time of submission, authors are requested to clearly specify whether their
submission is original or already published.
All submissions must be in PDF format, do not exceed 10 pages, and should be
written in Latex, using the standard Article style, 11pt.
All submissions will be reviewed by at least three members of the
program committee.
Papers accepted at the workshop will be electronically published on the
workshop web site.
Final and detailed submission instructions will be available on the workshop
web site soon.
IMPORTANT DATES
* Abstract submission deadline: 1 September 2008
* Papers submission deadline: 15 September 2008
* Notification of acceptance/reject: 25 October 2008
* Final version due: 15 November 2008
* Workshop: Around 9-13 December 2008
SELECTION FOR POST-PROCEEDINGS
(special issue of Elsevier J. of Algorithms in Logic, Informatics and Cognition)
* Extended papers submission deadline: 15 January 2009
* Notification of reviews of the 1st round: 28 February 2009
* Re-submission deadline
(for papers not accepted with minor rev.): 15 April 2009
* Final notification of acceptance: 1 May 2009
* Final version due: 15 May 2009
|
| | | | |
| | |
| |
Second Call for Papers
SymCon'08
The Eighth International Workshop
on Symmetry in Constraint Satisfaction Problems
(http://www.aloul.net/symcon)
To be held at the Fourteenth International Conference
on Principles and Practice of Constraint Programming (CP 2008)
Sidney, Australia
September 15th 2008
================================================================
WORKSHOP DESCRIPTION
--------------------
SymCon'08 is the 8th in a series of workshops affiliated with the CP conference,
and focuses on the investigation of symmetry and symmetry breaking techniques
for Constraint Satisfaction Problems (CSPs). Symmetries occur frequently in
CSPs. When undetected, they cause thrashing during traditional backtracking
search by redundantly exploring symmetric parts of the search space. The topic
was discussed as far back as 1874 by Glaisher, and new techniques to detect
and/or break symmetry have been proposed in recent years. However, many
outstanding problems remain. For instance, the detection and exploitation of
local, dynamic, and weak forms of symmetry remains a challenge.
The workshop is a forum for researchers to present advances in
symmetry breaking
techniques and to discuss the above or other open problems. Additionally, the
workshop welcomes the presentation of applications and case studies
that exhibit
some form of symmetry. The workshop is relevant to the computational group
theory (CGT) community because CGT is often the theory underlying many symmetry
breaking techniques.
Importantly, the organizers welcome submissions from researchers working in
other areas of Artificial Intelligence who feel that their work would be of
interest to the CP community. Such areas include planning, model checking, QBF
formulas, finite model search, and theorem proving in FOL.
Workshop topics include, but are not limited to:
- Symmetry definition: semantic symmetry, syntactic symmetry, constraint
symmetry, solution symmetry
- Automatic symmetry detection: static approaches and dynamic approaches
- Global symmetry detection and elimination
- Dynamic symmetry detection and elimination
- Combining symmetry breaking techniques
- Exploiting weak forms of symmetries like "dominance" and "almost-symmetries"
- Case studies of problems that exhibit interesting symmetries
- Application of computational group theory techniques to symmetry breaking
- Heuristics that use information about symmetry to guide search
- Elimination and avoidance of symmetry by re-modelling
- Dynamic avoidance of symmetric states during search
- Complexity analysis of symmetry breaking techniques
- Application of CSPs to symmetry and related algebraic problems
- Comparing symmetry breaking techniques in constraint programming
with techniques for dealing with symmetry in other search domains
- Symmetry in CNF formulas and OBF formulas
- Symmetry in finite model search in first order logic
- Novel exploitation of symmetry in varied search domains of interest
to the CP community
IMPORTANT DATES
---------------
Submission deadline: Sunday, 29th June 2008
Notification of acceptance: Thursday, 17th July 2008
Camera ready deadline: Sunday, 3rd August 2008
Workshop: Monday, 15th September 2008
PROGRAM COMMITTEE CHAIRS
------------------------
- Fadi Aloul
American University of Sharjah, UAE
Email: faloul@aus.edu
- Belaid Benhamou
University of Provence (Aix-Marseille I)
LSIS-CMI, 39 F. Joliot-Curie
13453 Marseille Cedex13 France.
Email: Belaid.Benhamou@cmi.univ-mrs.fr
- Lakhdar Sais
University of Artois
Rue Jean Souvraz SP-18
F-62307 Lens Cedex 3, France
E-mail : sais@cril.fr
|
| | | | |
| | |
| |
CALL FOR PAPERS
LPAR'08
15th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning
November 23-27, 2008
Carnegie Mellon University
Doha, Qatar
http://www.qatar.cmu.edu/lpar08
The series of International Conferences on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR) is a forum where, year after
year, some of the most renowned researchers in the areas of
automated reasoning, computational logic, programming languages and their
applications come to present cutting-edge results, to discuss advances
in these fields, and to exchange ideas in a scientifically emerging part
of the world. The 2008 edition will be held in Doha, Qatar, on the
premises of the Qatar campus of Carnegie Mellon University.
Submission:
-----------
There are short and long papers. See the web page for more information.
Important Dates
---------------
Abstract submission deadline: 26 May 2008
Paper submission deadline: 06 June 2008
Notification of acceptance: 29 August 2008
Camera-ready papers: 19 September 2008
Short paper submission deadline: 26 September 2008
LPAR'08 Workshops: 22 November 2008
LPAR 2008: 23-27 November 2008
|
| | | | |
| | |
| | | In case you have not noticed, in 2008 there is a new incarnation of the
hardware model checking competition (HWMCC'08). If you have
benchmarks in BLIF, SMV, VERILOG, or even AIGER, please
consider to submit them to the competition. We are also looking
for fair cycle respectively liveness properties this time. And last
but not least prepare your model checker to be submitted
as well.. In particular, note the qualification round deadline at the end
of this month (May 30). Final submission deadline is June 13. |
| | | | |
| | |
| |
------------------------------------------------------------------------
ASPL'08 -- Call for papers
------------------------------------------------------------------------
ASPL'08 -- The First Workshop on Analyses of Software Product Lines
(co-located with SPLC'08)
Limerick, Ireland, September 12, 2008
http://www.isa.us.es/aspl08
Submission Deadline: June 15, 2008
------------------------------------------------------------------------
MOTIVATIONS & OBJECTIVES
The automation of software product line (SPL) analyses is of growing interest to both practitioners
and researchers. In particular, automated analyses of variability models (like feature or decision
models) and languages that foster declarative specifications of programs using those models are now
common. We note that many of the problems that SPL engineers face are related to configuration
problems that have been addressed by the Artificial Intelligence (AI) community. Indeed, the SPL
community is using some of their results, e.g., BDD, CSP and SAT solvers.
This workshop is intended to bring together researchers in SPL and AI in order to review and discuss
synergies of the various approaches, and to propose new ideas and results. The two long term
objectives are (i) learn from what has been done up to now in AI that is related to automated
analyses of SPLs and (ii) creating a community interested in automated analyses of SPL in order to
keep SPL tools and research up-to-date with the latest technologies.
IMPORTANT DATES
- Submission Deadline: June 15, 2008
- Notification of Acceptance: July 18, 2008
- Camera Ready Versions Due: July 27, 2008
- ASPL'08 in Limerick: September 12, 2008
|
| | | | |
| | |
| | | SECURWARE 2008, The Second International Conference on Emerging Security Information, Systems, and Technologies.
August 25-31, 2008 - Cap Esterel, France.
General page: http://www.iaria.org/conferences2008/SECURWARE08.html;
Call for Papers: http://www.iaria.org/conferences2008/CfPSECURWARE08.html;
Submission deadline: April 15, 2008 |
| | | | |
| | |
| |
LaSh08 - WORKSHOP ON LOGIC AND SEARCH
Computation of structures from declarative descriptions
Call For Papers
Leuven, Belgium, November 6-7, 2008
http://www.cs.kuleuven.be/~dtai/LaSh08
................................................................
IMPORTANT DATES:
Submission: August 15, 2008
Notification: September 15, 2008
Workshop: November 6-7, 2008
|
| | | | |
| | |
| | | Dear all,
We are pleased to announce the call for benchmarks and solvers for the MaxSAT Evaluation 2008, http://www.maxsat.udl.cat/.
This year, there will be several changes to the MaxSAT evaluation:
1. You are asked to register on the MaxSAT evaluation web site before submitting a solver or benchmarks. A code will then be provided, that can be used for future submissions (as many as you like, until the deadline).
2. The file formats of the previous evaluation will be accepted. However, benchmarks may be provided in new formats, aiming smaller file sizes. The new formats which will soon be available at the MaxSAT evaluation website. Benchmarks can be submitted in any format, and they will be translated as required. All solvers should be able to read last year's formats.
3. For registering benchmarks, and in additional to the category (maxsat, partial maxsat, weighted maxsat, and weighted partial maxsat), you need to select the benchmark class. A benchmark can belong to any of the three following classes:
a. Random, if it is artificially created without any structure;
b. Crafted, if it is artificially created but has some structure;
c. Industrial, if it is not artificially created.
The schedule for the MaxSAT evaluation will be the following:
A. The deadline for the first submission will be in March 9th.
B. Afterwards, there will be a week for fixing solver bugs, using instances that will be provided for this purpose.
C. March 16th will be the final submission deadline for corrected solvers.
D. Afterwards the MaxSAT evaluation will take place.
Feel free to distribute this e-mail to anyone interested on submitting benchmarks or solvers to the MaxSAT evaluation.
---
MaxSAT Evaluation organizers |
| | | | |
| | |
| | | | | | | | Date: | 11-Jan-2008 | | Title: | IFIP AI 2008 — The Second IFIP International Conference on Artificial Intelligence in Theory and Practice
| | Hits: | 876 | | Contributed by: | | | | | | | | | Date: | 03-Dec-2007 | | Title: | Call For Participation: SAT Race 2008
| | Hits: | 1338 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Verification, Alternative approach, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, SAT tools, CSP, binary clause reasoning, SAT-solver, null |
| | | | | | |
| |
----------------------------------------------------------------
Announcement / Call for Participation
*************************
***** SAT-Race 2008 *****
*************************
(http://www-sr.informatik.uni-tuebingen.de/sat-race-2008)
May 12-15, Guangzhou, P. R. China
Affiliated with the SAT 2008 conference.
----------------------------------------------------------------
SAT-Race 2008 is a competitive event for solvers of the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event
to the Eleventh International Conference on Theory and Applications
of Satisfiability Testing (SAT'08) and stands in the tradition
of the yearly SAT Competitions that have been held since 2002
and the first SAT-Race held in 2006 in Seattle. In contrast
to the SAT Competitions, the focus of SAT-Race is on industrial
benchmarks only. Moreover, the time to solve each instance is
limited to 15 minutes.
Objective
---------
The area of SAT Solving has seen tremendous progress over the
last years. Many problems (e.g. in hardware and software
verification) that seemed to be completely out of reach a decade
ago can now be handled routinely. Besides new algorithms and
better heuristics, refined implementation techniques turned
out to be vital for this success.
To keep up the driving force in improving SAT solvers, we want
to motivate implementors to present their work to a broader
audience and to compare it with that of others.
Design and Organization
-----------------------
Researchers from both academia and industry are invited to
submit their solvers - in either source code or binary format -
to SAT-Race 2008. During SAT-Race, all entrants will have to
solve a set of benchmark instances in DIMACS CNF format that
will be drawn randomly from a pool of SAT instances. This pool
will mainly consist of benchmarks from previous SAT Competitions
(Industrial Category) and the SAT-Race 2006 pool, but may be
extended with additional instances of practical relevance.
The exact benchmark set will not be published in advance; a set
of similar benchmark instances will be made available for testing
purposes, however.
For each instance and solver there will be a time limit of 15
minutes. We will also organize qualification rounds, where
participation in at least one of them is mandatory to qualify
for the SAT-Race.
Assessment of solvers will be based on the number of
successfully handled instances and the time needed to solve
them.
There will also be two special tracks for:
* Parallel SAT Solvers (SMP, Multi-Threaded) and
* Structural SAT Solvers taking And-Inverter-Graphs (AIGs)
as input.
Details of the modus operandi and about the special tracks
are published on the web under
http://www-sr.informatik.uni-tuebingen.de/sat-race-2008.
Important Dates
---------------
- January 15, 2008: Deadline for registering solvers.
- February-March 2008: Qualification phase; exact dates of the
qualification rounds will be published on the web.
- March 31, 2008: Deadline for submitting final versions of
solvers.
- May 12-15, 2008: Announcement of results on the SAT 2008
conference.
Organizing Committee
--------------------
Chair
Carsten Sinz (Universitaet Tuebingen, Germany)
Advisory Panel
Nina Amla (Cadence Design Systems, USA)
Toni Jussila (OneSpin Solutions, Germany)
Daniel Le Berre (Universite d'Artois, France)
Panagiotis Manolios (Georgia Institute of Technology, USA)
Lintao Zhang (Microsoft Research, USA)
|
| | | | |
| | |
| | | | | | | | Date: | 14-May-2007 | | Title: | First Workshop on Autonomous Search
| | Hits: | 1012 | | Contributed by: | | | | CALL FOR PAPERS: second workshop on the Integration of SAT/SMT and CP techniques
http://research.microsoft.com/constraint-reasoning/Workshops/SAT-SMT-CP07/
a workshop of the CP 2007 Conference
http://www.cp2007.org/
DEADLINE FOR PAPER SUBMISSIONS:
June 29
WORKSHOP DESCRIPTION:
The techniques used in SAT (propagation, activity-based heuristics, conflict analysis, restarts...) constitute a very successful combination that makes modern DPLL solvers robust enough to solve large real-life instances without the heavy tuning usually required by CP tools. State-of-the-art SMT solvers build on these techniques, and are developed by extending SAT solvers with extra decision procedures for non-Boolean theories, such as the integers, the real numbers, or the un-interpreted functions. The reasoning on these non-Boolean theories can benefit from the experience acquired in CLP/CP, where very diverse constraint domains have traditionally been considered (constraints on finite domains, rational terms, real numbers, lists, graphs, etc.). Conversely, SMT brings new blood to a number of CP research areas, in particular to solver cooperation: the problems considered in SMT mix Boolean, numerical and symbolic domains, and SMT solvers are cooperative solvers that integrate a number of novel features, of which the most important is perhaps the use of a SAT solver as a central component in charge of “orchestrating” the cooperation. The goal of this workshop is to boost the discussions between the SAT/ SMT and CP communities by encouraging submissions at the border of these areas.
This forum will welcome the submission of papers related to all aspects of SAT/SMT or CP in which experience from one area benefits the other areas, as well as papers which, more generally, contribute to the integration between SAT/SMT and CP. Typical topics include, but are not restricted to:
- SAT-inspired and SMT-inspired improvements of CP techniques
- CP-inspired improvements of SAT and SMT techniques
- data structures and implementation issues
- constraint propagation and theory propagation
- pseudo-Boolean constraints and decision procedures for numerical theories
- clause learning and nogood-recording
- literal, variable and value heuristics
- integration of Boolean constraints and other types of constraints
- SAT encodings and conversions between CP/SAT format
- extensions of the SAT decision framework (handling of optimisation problems, etc.)
- solver cooperation and integration of procedures for different theories
- comparative studies that help understanding the respective strengths and privileged application areas of SAT, SMT and CP
|
| | | | |
| | |
| | | ----------------- Last Call for Papers -------------------
SMT Workshop '07
<5th International Workshop on Satisfiability Modulo Theories
Previously called: Pragmatics of Decision Procedures
in Automated Reasoning (PDPAR)
Berlin, Germany, 1-2 July 2007 (affiliated with CAV '2007)
http://www.lsi.upc.edu/~oliveras/smt07
======================================================================
AIMS AND SCOPE
The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Continuing with the PDPAR tradition, we
especially encourage submission of papers focused on pragmatic
aspects. Relevant topics include but are not limited to:
- New decision procedures and new theories of interest
- Combination of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Applications and case studies
- Theoretical results
IMPORTANT DATES
- Submission deadline : 23 April
- Notification of acceptance/rejection : 21 May
- Final version due : 4 June
- Workshop : 1-2 July
PROCEEDINGS
Given the informal style of the workshop, only informal proceedings
will be distributed at the workshop. We are planning to publish a
selected subset of the submitted papers as post-proceedings in a
special volume of the Electronic Notes in Theoretical Computer Science
(ENTCS) unless the authors prefer not to.
PAPER SUBMISSION
Following the PDPAR'06 initiative, there are two categories of
submissions:
- Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission.
- Presentation-only papers: describe work recently published or
submitted and will not be included in the proceedings.
Papers in both categories will be peer-reviewed. Full
submission guidelines are at the workshop web page.
INVITED SPEAKERS
- Rupak Majumdar, University of California, Los Angeles.
- Peter O'Hearn, Queen Mary, University of London.
STUDENT TRAVEL AWARDS
SMT 2007 will partially reimburse some students for their
conference-related expenses. Preference will be given
to students playing an active role in the workshop. However,
students in other situations are also encouraged to apply.
We require applications in the form of a short recommendation letter
written by the student's supervisor, to be sent to the PC chairs by
May 28.
PROGRAM CHAIRS
- Sava Krstic, Intel Corporation
- Albert Oliveras, Tech. Univ. of Catalonia
PROGRAM COMMITTEE
- Clark Barrett, New York University
- Alessandro Cimatti, ITC-Irst, Trento
- Byron Cook, Microsoft Research
- Amit Goel, Intel Corporation
- Aarti Gupta, NEC Labs America
- Shuvendu Lahiri, Microsoft Research
- Leonardo de Moura, Microsoft Research
- Robert Nieuwenhuis, Technical University of Catalonia
- Silvio Ranise, LORIA, Nancy
- Roberto Sebastiani, Universita` di Trento
- Ofer Strichman, Technion
- Cesare Tinelli, University of Iowa
- Ashish Tiwari, Stanford Research Institute (SRI)
|
| | | | |
| | |
| | Call For Model Checkers and Benchmarks
Hardware Model Checking Competition 2007 (HWMCC'07)
http://fmv.jku.at/hwmcc
HWMCC'07 is the first competitive event for model checkers similar in
spirit to the SAT competition. It is organized as a satellite event to
the 19th International Conference on Computer Aided Verification (CAV'07).
Model checking of hardware is not only an active research area, but also
is widely applied in industry. To keep up the driving force in
improving model checkers, we want to motivate implementors to present
their work to a broader audience and collect benchmarks.
Researchers from both academia and industry are invited to submit
benchmarks and solvers to HWMCC'07. In the competition all entrants will
have to solve a set of benchmark instances in AIGER format
(http://fmv.jku.at/aiger). The AIGER format report also describes the
input and output requirements.
Important Dates
April 13, 2007: Deadline for registering solvers.
April 20, 2007: Deadline for submitting benchmarks.
April 30, 2007: Start of qualification rounds.
June 1, 2007: Start of competition.
June 29, 2007: End of competition.
July 2, 2007: Ranking of results.
July 3-7, 2007: Presentation of results.
Chairs
Armin Biere (Johannes Kepler University, Linz, Austria)
Toni Jussila (Johannes Kepler University, Linz, Austria)
Competition Committee
Alessandro Cimatti (IRST, Trento, Italy)
Koen Lindstrom Claessen (Chalmers University, Gothenburg, Sweden)
Ken McMillan (Cadence Berkeley Labs, Berkeley, USA)
Fabio Somenzi (University of Colorado, Boulder, USA) |
| | | | |
| | |
| | | SMT Workshop '07
5th International Workshop on Satisfiability Modulo Theories
Previously called: Pragmatics of Decision Procedures
in Automated Reasoning (PDPAR)
Berlin, Germany, 1-2 July 2007 (affiliated with CAV '2007)
======================================================================
BACKGROUND
Deciding the satisfiability of first-order formulas modulo background
theories, known as the Satisfiability Modulo Theories (SMT) problem,
has proved to be useful in verification, compiler optimization,
scheduling, and other areas.
The success of SMT techniques depends on the
development of both domain-specific decision procedures for each
concrete theory (e.g. linear arithmetic, the theory of arrays, or the
theory of bit-vectors) and combination methods that allow one to
obtain more versatile SMT tools. These two ingredients together make
SMT techniques well-suited for use in larger automated reasoning and
formal verification efforts.
AIMS AND SCOPE
The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Continuing with the PDPAR tradition, we
especially encourage submission of papers focused on pragmatic
aspects. Relevant topics include but are not limited to:
- New decision procedures and new theories of interest
- Combination of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Applications and case studies
- Theoretical results
IMPORTANT DATES
- Submission deadline : 23 April
- Notification of acceptance/rejection : 21 May
- Final version due : 4 June
- Workshop : 1-2 July
Full submission guidelines available at the workshop web page:
www.lsi.upc.edu/~oliveras/smt07 |
| | | | |
| | |
| | The third Pseudo-Boolean evaluation (PB'07) is organized as a special event
of the SAT 2007 conference. Like the previous evaluations (PB'05, PB'06),
the goal is to assess the state of the art in the field of pseudo-Boolean
solvers.
This year's evaluation introduces a call for non-linear pseudo-Boolean
solvers and benchmarks. Tools will be provided to convert non-linear
constraints for linear solvers.
The deadline for submitting benchmarks or solvers is fixed to February 16, 2007.
Other deadlines as well as the evaluation rules are available at
http://www.cril.univ-artois.fr/PB07/
We would particularly appreciate the submission of
* linear and non-linear pseudo-Boolean solvers
* industrial benchmarks
* benchmarks generators
* benchmarks sets with a wide distribution of their number of clauses, cardinality constraints and pseudo-Boolean constraints
* non-linear pseudo-Boolean benchmarks
|
| | | | |
| | |
| | | QBFEVAL 2007 is the second competitive evaluation of QBF solvers, and the fifth evaluation of QBF solvers and instances ever. The previous QBFEVAL was the first competitive one, and also the one attracting the highest number of participants so far. QBFEVAL 2007 will award solvers that stand out as being particularly effective on specific categories of QBF instances and instances that turn out to be particularly hard to solve given the current state of the art. See the website for more information or contact the organizers using the address qbf07_AT_qbflib.org. |
| | | | |
| | |
| | | | | | | | Date: | 12-Oct-2006 | | Title: | 2nd Call for papers: JSAT special issue on Satisfiability Modulo Theories
| | Hits: | 958 | | Contributed by: | | | | | | | | | Date: | 12-Oct-2006 | | Title: | SAT 2007 Call For Paper: deadline for submission is January 19, 2007
| | Hits: | 1529 | | Contributed by: | Daniel Le Berre | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Quasigroups, Local Search, Random 3SAT, Complexity, Randomization, Verification, Alternative approach, QBF, Structure of problems, Benchmark, SAT application, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, SAT tools, branching heuristics, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, SAT-Based, Lookahead, Stochastic Satisfiability, SAT-Solver Competition, SAT/CP |
| | | | | | |
| |
SAT 2007
Call for Papers
10th International Conference on
Theory and Applications of Satisfiability Testing
May 28 - 31, Lisbon, Portugal
http://sat07.ecs.soton.ac.uk
The International Conference on Theory and Applications of
Satisfiability Testing is the primary annual meeting for researchers
studying the propositional satisfiability problem (SAT). SAT'07 is
the tenth SAT conference. SAT'07 features the SAT competition, the
QBF competition, the Pseudo-Boolean evaluation, and the MAX-SAT
evaluation.
SCOPE
Many hard combinatorial problems can be encoded into SAT.
Therefore improvements on heuristics on the practical, as well as
theoretical insights into SAT apply to a large range of real-world
problems. More specifically, many important practical verification
problems can be rephrased as SAT problems. This applies to
verification problems in hardware and software. Thus SAT is becoming
one of the most important core technologies to verify secure and
dependable systems. The topics of the conference span practical and
theoretical research on SAT and its applications and include but are
not limited to proof systems, proof complexity, search algorithms,
heuristics, analysis of algorithms, hard instances, randomized
formulae, problem encodings, industrial applications, solvers,
simplifiers, tools, case studies and empirical results. SAT is
interpreted in a rather broad sense: besides propositional
satisfiability, it includes the domain of quantified boolean
formulae (QBF), constraints programming techniques (CSP) for
word-level problems and their propositional encoding and
particularly satisfiability modulo theories (SMT).
SUBMISSION
Submissions should contain original material and can either be
regular research papers up to 14 pages or short papers up to 6
pages. Double submissions including submissions as short and long
papers will be rejected. Submissions should use the Springer
LNCS style. All appendices, tables, figures and the bibliography
must fit into the page limit. Submissions deviating from these
requirements may be rejected without review. All accepted papers
including short papers will be published in the proceedings of the
conference. The conference proceedings will be published within
Springer LNCS series. The submission page is
http://www.easychair.org/SAT2007. Papers have to be submitted
electronically as PDF files. Paper submissions are due by January 19.
PROGRAM CHAIRS
Joao Marques-Silva, University of Southampton, UK
Karem Sakallah, University of Michigan, USA
LOCAL CHAIR
Ines Lynce, Technical University of Lisbon, Portugal
IMPORTANT DATES
January 19, Paper Submission
March 2, Author Notification
March 16, Final Version
More information on the conference web site. |
| | | | |
| | |
| | CALL FOR EXTENDED ABSTRACTS
International Symmetry Conference
http://isc.dcs.st-and.ac.uk
To be held in the Thistle Hotel, Edinburgh
14th to the 17th of January, 2007
Conference Description
This conference focuses on current symmetry research in the areas of Constraint Programming, Boolean Satisiability, Group Theory, Model Checking, Planning, and any other combinatorial research area.
The objective is to promote discussion and presentation of novel ideas relating to symmetry within the above areas, and to foster new collaboration opportunities between areas. This will be achieved by presentations of current work both in individual areas and of a collaborative nature.
Conference Format
This conference is open to all members of the combinatorial research communities. The conference will emphasize discussion and cross-fertilization, so presentations will be balanced with discussion time, tutorials and invited talks. In this direction, the conference is seeking high quality papers that address cutting-edge research in this field, and that can contribute to the discussion.
The agenda will include:
- Tutorial time at the start, to introduce each area and the role symmetry plays within it to a general audience.
- An invited speaker from each area of to talk about recent research on a topic of their choice.
- Presentations and posters of the accepted Extended Abstracts.
- A competition which will allow different techniques to tackle one problem.
- A doctoral program, where the best abstracts will be invited for presentation and the remaining abstracts will be allocated a poster. There will also be a mentoring session where Doctoral students will be paired with a more senior researcher from a different area.
Important Dates
Submission Deadline: October 16th, 2006
Notifications to Authors: November 6th, 2006
Final Version Deadline: December 11th, 2006
Early Registration Deadline: TBA
Conference: January 14th to January 17th, 2007 |
| | | | |
| | |
| | | All are invited to the 2006 Symposium on Satisfiability Solvers and Program Verification (SSPV). Seattle, August 10 - 11. SSPV is a FLoC event. We have invited the following researchers to come speak about new work in the intersection between program verification and SAT-solvers.
Alex Aiken, Stanford
Title: Scalable Program Analysis Using Boolean Satisfiability
Alessandro Cimatti, IRST
Title: Reasoning about Bit Vector programs with Decision Procedures
Edmund Clarke, CMU
Title: Bounded and Unbounded Model Checking using SAT
Carla Gomes, Cornell
Title: Beyond Satisfiability: Model Counting, Quantification, and Randomization
Aarti Gupta, NEC
Title: Verifying C Programs using SAT-based model checking
Orna Grumberg, Technion
Title: Hybrid BDD and All-SAT Method for Model Checking
Daniel Kroening, ETH
Title: SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic
Shuvendu Lahiri, Microsoft Research
Title: Efficient SAT-based Techniques for Predicate Abstraction
Sharad Malik, Princeton
Title: Optimization and Relaxation in SAT Search
Ken McMillan, Cadence Labs
Title: SAT, interpolants, and software model checking
Roberto Nieuwenhuis, Technical University of Catalonia
Title: The new architecture and solvers in the Barcelogic tool for SAT modulo theories.
Ofer Strichman, Technion
Title: Decision Heuristics based on an Abstraction/Refinement model
Sponsored by the Institute for Pure and Applied Mathematics (IPAM).
Organizers: Dimitris Achlioptas, Byron Cook, Moshe Vardi |
| | | | |
| | |
| | September 25th 2006, Nantes, France
The interest of the community on preferences and soft constraints has increased in the last years. Examples are, from the modeling side, an active research on CP nets and some preference-based logic, and from the algorithmic side, several studies dealing with specific semantics of soft constraints such as propositional logic formulae (i.e. MAX-SAT) or global soft constraints in Constraint Programming or probability distributions (i.e. probabilistic reasoning) or uncertainty.
The purpose of this workshop is to bring together researchers and practitioners who are interested in all aspects of preferences and soft constraints, such as:
* theoretical frameworks
* problem modeling
* solving algorithms
* decomposition methods and associated graph algorithms
* tractability
* languages
* preference aggregation
* preference elicitation
* multi-objective or qualitative optimization
* combining/integrating different frameworks and algorithms
* comparative studies
* real-life applications
This year, the workshop is more specifically oriented towards graph decomposition approaches and tractability. Papers presenting new decomposition approaches, original criteria for selecting a decomposition, algorithms for generating interesting decompositions, comparison with existing approaches, theoretical and practical issues on the exploitation of such decompositions, new tractable classes... are especially welcome.
Important Dates:
* Paper Submission deadline: July 2nd
* Notification of acceptance: July 22th
* Workshop Date: September 25th
|
| | | | |
| | |
| | |
| | We’d like to welcome submissions for the following workshop:
The CP 2006 Workshop on the
Integration of SAT and CP techniques
September 25, 2006, Nantes, France
Workshop Description
SAT and CP techniques are two problem solving technologies which share many similarities, and there is considerable interest in cross-fertilising these two areas. The techniques used in SAT (propagation, activity-based heuristics, conflict analysis, restarts...) constitute a very successful combination which makes modern DPLL solvers robust enough to solve large real-life instances without the heavy tuning usually required by CP tools. Whether such techniques can help the CP community develop more robust and easier-to-use tools is an exciting question. One limitation of SAT, on the other hand, is that not all problems are effectively expressed in a Boolean format. This makes CP an appealing candidate for many applications, like software verification, where SAT is traditionally used but more expressive types of constraints would be more natural. The goal of this workshop is to boost the discussions between the SAT and CP communities by encouraging submissions at the border of these two areas.
We welcome the submission of papers related to any aspect of SAT or CP in which experience from one area benefits the other area, as well as papers which, more generally, contribute to the integration between SAT and CP. Typical topics include, but are not restricted to:
- SAT-inspired improvements of CP techniques
- CP-inspired improvements of SAT techniques
- data structures and implementation issues
- propagation algorithms
- pseudo-Boolean constraints
- clause learning and nogood-recording
- literal, variable and value heuristics
- integration of Boolean constraints and other types of constraints
- handling of non-Boolean domains in verification applications
- SAT encodings and conversions between CP/SAT format
- extensions of the SAT decision framework (Satisfiability Modulo Theories, handling of optimisation problems, etc.)
Submission procedure
We ask authors to submit technical papers either in Postscript or PDF using the CP conference style. A limit of 15 pages is required. Please submit papers to youssefh_at_microsoft_dot_com. The deadline is June 18th. See the
webpage of the workshop for more details. |
| | | | |
| | |
| | | Affiliated with ICLP-06, at FLoC-06 (and just after SAT-06), will be a workshop
Search and Logic: Answer Set Programming and SAT. The call for papers, and other
details, can be found on the workshop web page: http://www.cs.sfu.ca/~SearchAndLogic/.
Invited speakers include Henry Kautz and Mirek Truszczynski. We also plan tutorials
on related topics, and regular paper sessions. Submission deadline is May 22. |
| | | | |
| | |
| | | AAAI, the main North American AI conference, now has a track for presentation
of work that represents "highlights" of work in related areas, presented at other
(not necessarily AI) conferences, which would be of interest to AAAI participants.
Papers are short (4 pages max) summaries of one or more papers published in the
last year or two. Please consider submitting. Feel free to write me (or any other
Nectar track PC member) if you are unsure if your work would be of interest to AAAI.
Please also consider suggesting work by other researchers that deserves
presentation to a wider audience.
The deadline for submissions is March 14, but since the papers are short summaries,
preparation should not be to onerous. Further details can be found at:
http://www.aaai.org/Conferences/AAAI/2006/aaai06nectar.php |
| | | | |
| | |
| | The second Pseudo-Boolean evaluation is organized as a special event of
the SAT 2006 conference.
It follows the first
Pseudo-Boolean evaluation which gathered together 8 solvers. The
goal of this evaluation is to assess the state of the art in
the field of pseudo-Boolean solvers.
The deadline for submitting benchmarks or solvers is fixed to April 16, 2006.
Other deadlines as well as the evaluation rules are available on
http://www.cril.univ-artois.fr/PB06
We would particularly appreciate the submission of
- pseudo-Boolean solvers
- industrial benchmarks
- benchmarks generators
- benchmarks sets with a wide distribution of their number of
clauses, cardinality constraints and pseudo-Boolean constraints
|
| | | | |
| | |
| | | The final CFP for SAT 2006 includes revised submission dates. |
| | | | |
| | |
| |
Call for Participation
Second International Summer School of the
Association for Constraint Programming
Advanced School and International Workshop on
GLOBAL CONSTRAINTS
Doryssa Bay Hotel
Samos, Greece
June 18-23, 2006
http://www.cse.unsw.edu.au/~tw/school.html
The Second International Summer School on Constraint Programming is an
advanced school and associated workshop on global constraints. The school
and workshop are aimed at PhD students, researchers, and practitioners of
all levels who wish to learn about this key area in depth. A workshop
will run alongside the school where the very latest research results
in global constraints will be presented. Lecturers include:
Philippe Baptisite, Nicolas Beldiceanu, Christian Bessiere, Mats Carlsson,
Willem-Jan van Hoeve, Irit Katriel, Michela Milano, and Jean-Charles Regin.
The school and workshop will take place in the Doryssa Bay hotel on the
Aegean island of Samos in Greece. The hotel is next to the fishing
village of Pythagorion, the birth place of the Greek philosopher
Pythagoras.
To participate in the advanced school and workshop, please email Toby Walsh
(tw@cse.unsw.edu.au) as soon as possible. As places are limited, you are
encouraged to reserve a place as soon as possible. The early registration
fee will be approximately 300 euros. Student grants will be available to
cover part of the expenses of some students. More details are
available at http://www.cse.unsw.edu.au/~tw/school.html
|
| | | | |
| | |
| | | | | | | | Date: | 10-Nov-2005 | | Title: | CSR-2006 International Computer Science Symposium in Russia
| | Hits: | 2321 | | Contributed by: | Daniel Le Berre | | Keywords: | Deduction Rules, DPLL, DP, Minimal models, Intelligent Backtracking, Local Search, Random 3SAT, Complexity, Computational logic, QBF, SAT application, Equivalency Reasoning, Learning, Model Elimination, SAT tools, Logic, QBF, General Interest, conference information |
| | | | | | |
| |
CSR-2006
International Computer Science Symposium in Russia
Sponsored by the U.S. Civilian Research & Development Foundation
Organized by St.Petersburg Department of Steklov Institute of Mathematics
June 8-12, 2006, St.Petersburg, Russia
Final Call for Papers
CSR 2006 is the first conference in a series of regular events intended
to reflect the broad scope of international cooperation in computer
science. CSR 2006 consists of two tracks:
Theory Track:
* algorithms, protocols, and data structures;
* complexity and cryptography;
* formal languages, automata and their applications to computer science;
* computational models and concepts;
* proof theory and applications of logic to computer science.
Applications and Technology Track:
* programming and languages;
* computer architecture and hardware design;
* symbolic computing and numerical applications;
* application software;
* artificial intelligence and robotics.
Program committee:
Theory Track: Sergei Artemov, Paul Beame, Michael Ben-Or, Andrei Bulatov,
Peter Buergisser, Felipe Cucker, Evgeny Dantsin, Volker Diekert,
Dima Grigoriev (chair), Yuri Gurevich, Janos Makowsky, Yuri Matiyasevich,
Peter Bro Miltersen, Grigori Mints, Pavel Pudlak, Prabhakar Raghavan,
Alexander Razborov, Michael E. Saks, Alexander Shen, Amin Shokrollahi,
Anatol Slissenko, Mikhail Volkov
Applications and Technology Track: Boris Babayan, Robert Bauer, Matthias Blume,
Walter Daelemans, Vassil Dimitrov, Sergey Dmitriev, Richard Fateman,
Dina Goldin, John R. Harrison (chair), John Mashey, Bertrand Meyer,
Fedor Novikov, Michael Parks, Andreas Reuter, Mary Sheeran,
Elena Troubitsyna, Miroslav Velev, Sergey Zhukov
The (confirmed) invited speakers include:
* Boaz Barak (Princeton University, USA)
* Gerard Berry (Esterel Technologies, France)
* Bob Colwell (R&E Colwell & Assoc. Inc., USA)
* Byron Cook (Microsoft Research, USA)
* Melvin Fitting (Lehman College and the Graduate Center, CUNY, USA)
* Russell Impagliazzo (University of California at San Diego, USA)
* Michael Kaminski (Technion, Israel)
* Pascal Koiran (Ecole Normale Superieure de Lyon, France)
* Omer Reingold (Weizmann Institute, Israel)
The opening lecture will be given by Stephen A. Cook
(University of Toronto, Canada).
It is planned to publish the proceedings of the symposium in
Springer's LNCS series.
Important dates:
* Paper submission: December 11, 2005
* Notification: January 31, 2006
* Symposium: June 8-12, 2006
There will be limited support for travel expenses of Russian participants.
Further information and contacts:
Web: http://logic.pdmi.ras.ru/~csr2006/
Email: csr06chair@logic.pdmi.ras.ru
|
| | | | |
| | |
| | | All the data concerning the pseudo-boolean special track of the SAT 2005 competition is finally publicly available ! |
| | | | |
| | |
| | | | | | | | Date: | 02-Aug-2005 | | Title: | SAT 2005 Competition detailed results
| | Hits: | 2560 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Repository, Random 3SAT, Randomization, Verification, Structure of problems, EDA, Benchmark, SAT application, Randomised Algorithms, Instance simplification, Learning, SAT tools, branching heuristics, Dynamic restarts, Preprocessing, Unit Propagation |
| | | | | | |
| | |
| | From the workshop web site:
This workshop can be of interest to researchers working in all aspects of quantification in constraint programming and related areas such as SAT. The workshop's aim is to present a forum for researchers interested in quantification, and coming from diverse backgrounds (e.g. constraint satisfaction, SAT, logic, linear programming), to present results, exchange ideas and discuss future directions. Topics of interest include (but are not limited to):
- complexity results
- problem modelling
- search and propagation algorithms
- combining/integrating different frameworks and algorithms
- benchmark generation and evaluation methodology
- real-world applications of quantified constraints
|
| | | | |
| | |
| | | The new deadline is May, 9th.
This workshop will bring together practioners and researchers who are concerned with the implementation and deployment of working automated reasoning systems for classical logic (propositional, first order, and higher order). The focus is on classical logic because it has adequate expressive power for many applications, has well understood and manageable computational properties, and the automated reasoning community has much experience and success with the implementation and application of automated reasoning systems for classical logics. Consequently, there exist empirically successful classical automated reasoning systems and applications. The workshop will discuss "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software. The workshop will have two main topic areas: |
| | | | |
| | |
| | | | | | | | Date: | 31-Mar-2005 | | Title: | Final CFP for PDPAR'05 -- the CAV'05 affiliated Workshop on Pragmatics of Decision Procedures
| | Hits: | 2077 | | Contributed by: | | | | | | | | | Date: | 29-Sep-2004 | | Title: | Logic Summer School 2004 The Australian National University
| | Hits: | 2038 | | Contributed by: | | | | SAT is one of the topics in Track 1, AI.
The submission deadline is September 3, 2004. |
| | | | |
| | |
| | | Online registration for the SAT 2004 conference, to be held May 10-13 in Vancouver, BC, closes on
>>> Friday, 7 May 2004, 9:00 AM PDT <<< (Pacific daylight savings time).
Unfortunately, we cannot offer onsite registration for SAT 2004.
Holger Hoos and Dave Mitchell
SAT 2004 Co-chairs |
| | | | |
| | |
| | | The deadline for early registration for SAT 2004 as well as for the conference rate at the Renaissance Hotel is:
>>> 24 March 2004 <<< (today!)
Due to organisational constraints, this deadline cannot be extended. After 24 March 2004, room rates are likely to be substantially higher -- the regular room rate for the conference dates is 239 CAD / night, compared to the conference rate of 150 CAD / night.
The conference registration includes breakfasts and lunches -- details can be found at the conference webpage (http://www.satisfiability.org/SAT04), from where electronic registration and hotel booking is available.
A list of accepted papers and invited talks is also available at http://www.satisfiability.org/SAT04.
Don't miss out on this exciting event and the spectacular location!
We look forward to seeing you in Vancouver,
Holger H Hoos and David G Mitchell
SAT 2004 Co-chairs
PS: Please note that we cannot offer onsite registration. Late registration for SAT 2004
is expected to close 30 April 2004. |
| | | | |
| | |
| | | Online registration for the SAT 2004 conference is now open. The early registration rate applies until 24 March. (Due to hard organisational and contractual constraints, this deadline cannot be extended).
For further information see http://www.satisfiability.org/SAT04/.
We are looking forward to seeing you in Vancouver,
Holger & Dave |
| | | | |
| | |
| | | Electronic paper/poster registration for SAT 2004 is now open at http://www.satisfiability.org/SAT04.
All authors who plan to submit papers or posters should register their submissions before Tuesday, 2004/02/10 - this will help us in preparing the reviewer assignment for the actual submissions (due 2004/02/20).
Registration for the conference itself is expected to open next week, with early registration rates being offered until 2004/03/24. |
| | | | |
| | |
| | | SAT 2004 Paper, Solver and Benchmark submission deadlines have just
been extended. New dates are:
Author Registration (Paper/Solver/Benchmark): February 10;
Paper Submission: February 20;
SAT Solver/Benchmark Submission: February 23;
QBF Solver/Benchmark Submission: February 28;
Notification of Acceptance: March 19;
Early Registration: March 24;
Camera Ready Deadline: April 12;
Conference: May 10-13 |
| | | | |
| | |
| | | The objective of BMC'03 is to bring together scientists from academia and industry to report and debate advances in Bounded Model Checking and related issues.
Since its introduction in 1999 by Biere, Cimatti, Clarke and Zhu, Bounded Model Checking has been adopted by most relevant companies as a complementary technique to the more traditional BDD based unbounded symbolic model checking. Largely due to the advances in SAT technology in the last few years, Bounded Model Checking became a leading tool in detection of relatively shallow logical errors, outperforming BDD based tools in most of these cases. The large interest in this technology has created a constant stream of new ideas and improvements that make this technique more and more useful. In this workshop we hope to bring together all those people that are interested in this area to share their ideas and report their results.
The scope of the workshop includes all theoretical and practical aspects of Bounded Model Checking, including, but not limited to:
- Combining BMC with other tools and techniques (such as BDD’s)
- Experimental results in industrial settings
- Bounded model checking of infinite systems
- Translation schemes
- SAT techniques related to BMC
Important dates:
Submissions: April 27, 2003
Notification: June 2, 2003
Final papers: June 16, 2003
Workshop: July 13, 2003
|
| | | | |
| | |
| | | | | | | | Date: | 16-Dec-2002 | | Title: | First QBF solver evaluation
| | Hits: | 4113 | | Contributed by: | Daniel Le Berre | | Keywords: | Deduction Rules, Intelligent Backtracking, Data structure, Local Search, Complexity, Randomization, Alternative approach, QBF, Structure of problems, Benchmark, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Satisfiable Problems Generation, branching heuristics, phase transition, binary clause reasoning |
| | | | | | |
| | |
The purpose of the evaluation is to assess the current state of the art in the field of QBF solvers. Therefore, not only the submission of QBF solvers is welcomed, but also the submission of QBF formulas to be used as benchmarks for the evaluation.We strongly encourage people thinking about QBF-based techniques in their area (e.g., automated deduction, formal verification, planning and scheduling) to contribute to the evaluation by submitting QBF instances of their research problems.The results of the evaluation will be a good indicator of the current feasibility of the QBF-based approach and a stimulus for people working on QBF solvers to further enhance their tools.
Important dates:
- Deadline for submitting benchmarks and solvers: February 28, 2003
- Buggy solvers returned to the authors: February 10, 2003
- Buggy solvers resubmitted: March 16, 2003
- Evaluation: March 16 - May 5, 2003
- Results: May 5-8, 2003
|
| | | | |
| | |
| | | | | | | | Date: | 16-Dec-2002 | | Title: | The SAT competition 2003
| | Hits: | 4497 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, DP, Intelligent Backtracking, Data structure, Local Search, BDD, Random 3SAT, Complexity, Randomization, Alternative approach, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, branching heuristics, binary clause reasoning, Dynamic restarts |
| | | | | | |
| | | A new SAT solver competition is organized next year. If you missed the previous one, do not miss
this one!
Solvers and benchmarks are welcome!
Please take a look at the competition web page for details about the competition: submission policy, changes since last year competition, etc.
Important dates:
- February, 14: deadline for submitting benchmarks.
- February, 14: deadline for submitting solvers.
- February, 28: buggy solvers returned to the authors.
- March, 7: buggy solvers resubmitted.
- March, 14: 1st stage of the competition starts.
- April, 14 (or earlier): 2nd stage of the competition starts.
- May: results during SAT2003 conference, awards.
|
| | | | |
| | |
| | | | | | | | Date: | 16-Dec-2002 | | Title: | SAT & QBF 2003 conference
| | Hits: | 2559 | | Contributed by: | Daniel Le Berre | | Keywords: | BMC, DPLL, Minimal models, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Randomization, Verification, Alternative approach, QBF, Structure of problems, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, Dynamic restarts |
| | | | | | |
| | | The Sixth International Conference on Theory and Applications of Satisfiability Testing
will be held in S. Margherita Ligure-Portofino ( Italy), May 5-8 2003.
The conference follows the Workshops on Satisfiability held in Siena (1996), Paderborn (1998), and Renesse (2000), the Workshop on Theory and Applications of Satisfiability Testing held in Boston (2001) and the Symposium on Theory and Applications of Satisfiability Testing held in Cincinnati (2002).
The purpose of this conference is to bring together researchers from different communities -- including theoretical computer science, artificial intelligence, verification, mathematical theorem-proving, electrical engineering , and operations research -- in order to share ideas and increase synergy between theoretical and empirical work.
Please note that work on problems close to SAT (MAX-SAT,QBF, etc) are welcome.
Important dates:
- Extended abstracts submission: February 8, 2003
- Notification of acceptance: March 10, 2003
- Final version due: April 1, 2003
|
| | | | |
| | |
| | |
| | | | | | | | Date: | 30-Oct-2001 | | Title: | SAT2002: 5th International Symposium on the Theory and Applications of Satisfiability Testing
| | Hits: | 2396 | | Contributed by: | | | | | | | | | Date: | 27-Sep-2001 | | Title: | LICS2002 Symposium
| | Hits: | 1797 | | Contributed by: | | | | | | | | | Date: | 27-Aug-2001 | | Title: | Microprocessor Test and Verification (MTV'02), January 21-22, 2002, Austin, Texas, USA: Special sessions on optimizing SAT procedures for application to testing and formal verification.
| | Hits: | 2158 | | Contributed by: | Miroslav Velev | | Keywords: | Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, Satisfiable Problems Generation, SAT tools |
| | | | | | |
| | | The deadline for submission of abstracts was changed to: October 26, 2001. |
| | | | |
| | |
| | | Deadline for submission of abstracts: August 31, 2001. |
| | | | |
| | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
