 |
50 elements available | | | 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 |
| |  | |  |
| | |
| |
10th Workshop on Preferences and Soft Constraints, SofT'10
Held in conjunction with the 16th International Conference on
Principles and Practice of Constraint Programming, CP'10
Technical Description
---------------------
Preferences are ubiquitous in real life: most problems are
over-constrained and would not be solvable if we insist that all their
requirements are strictly met. Moreover, many problems are more
naturally described via preference rather than hard statements. Soft
constraints are the way the constraint community has extended its
classical framework to deal with the concept of preferences.
This workshop will bring together researchers interested in all
aspects of soft constraints and cost function processing, such as:
- theoretical frameworks
- problem modeling
- solving algorithms
- languages
- preference aggregation and elicitation
- multi-objective or qualitative optimization
- combining/integrating different frameworks and algorithms
- comparative studies
- real-life applications
The workshop is an opportunity to share knowledge between people
working in algorithms and solvers for formalisms, including
Weighted Max-SAT, Soft CSP, Bayesian Networks, Random Markov
Field, Factor Graphs, Pseudo Boolean Optimization, SAT Modulo
Theories, and related formalisms.
Workshop Format
---------------
This workshop is intended to build on the experience and success of
the CP'99 to CP'06 workshops on the same subject and the recent
meeting on cost function processing (25 attendees during two
days). Its aim is to provide a forum where researchers currently
working in this area can discuss their most recent ideas and
developments and think together about the most promising new
directions. Therefore, we encourage the presentation of work in
progress or on specialized aspects of preferences, soft constraints,
and more generally, cost function processing. Papers that bridge the
gap between theory and practice are especially welcome.
Paper Submission
----------------
Paper submissions should contain original material and must not exceed
15 pages. 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. Paper submission and reviewing will be done
via EasyChair. The paper submission page is:
http://www.easychair.org/conferences/?conf=soft10.
Important dates
----------------
Paper Submission June 18
Notification July 23
Final Versions August 8
Workshop Date September 6
Workshop Organizers
--------------------
Simon de Givry, INRA, Toulouse, France
Felip Manya, CSIC, Barcelona, Spain
Joao Marques-Silva, University College Dublin, Ireland
Program Committee
---------------------
Fahiem Bacchus, University of Toronto, Canada
Hachemi Bennaceur, CRIL, France
Stefano Bistarelli, University of Perugia, Italy
Jimmy Lee, Chinese Univ. of Hong Kong, China
Chu-Min Li, Université de Picardie, France
Ines Lynce, Technical Univ. of Lisbon, Portugal
Pedro Meseguer, CSIC, Spain
Thierry Petit, LINA-CNRS, France
Jordi Planes, Universitat de Lleida, Spain
Emma Rollon, Technical Univ. of Catalonia, Spain
Thomas Schiex, INRA, France
Francesca Rossi, University of Padova, Italy
Brent Venable, University of Padova, Italy
Gerard Verfaillie, ONERA, France
Tomas Werner, Czech Tech. Univ., Czech Republic
Nic Wilson, 4C, Ireland
|
| | | | |
| | |
| | 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. |
| | | | |
| | |
| |
====================================================================
SECOND CALL FOR PAPER
====================================================================
Call for papers
WPSS'2010
A workshop on
Parallel Satisfiability Solving:
SAT and beyond SAT,
Parallel Solving on New Architectures
as part of the HPCS'10 Conference
Le CENTRE DE CONGRES de CAEN
Caen, Normandy, France
June 28 -- July 2, 2010
http://cisedu.us/cis/hpcs/10/main/callForPapers.jsp
====================================================================
Submission Deadline: February 15, 2010
SCOPE AND OBJECTIVES
During the last decade, the fundamental Satisfiability Problem (SAT) has been extensively studied.
This interest of the community significantly grows because of its conceptual simplicity and its
ability to describe a wide set of various problems, including hardware verification, planning,
automated reasoning, and others. Consequently, there is an increasing demand for high performance
SAT-solving algorithms in industry. To date, the parallel SAT solving remains a challenging
problem. In spite of the actual trend in processor development, which is moving from single-core to
multi-core CPU, there exist few parallel solving works dedicated to the SAT problem. This workshop
will focus on SAT and beyond SAT solving techniques exploiting parallelism within a context of High
Performance Computing including massively parallel architectures such as Global Processing Units
(GPUs) and Field-Programmable Gate Arrays (FPGAs).
We invite papers in this emerging discipline which includes, but not limited to, the following areas
of interest.
- High Performance Computing for SAT, Max-SAT #SAT and QBF solving.
- General-Purpose Computation on GPUs (GPGPU) for SAT*
- Reconfigurable Computing and FPGA for SAT*
- Parallel SAT* Pre-processing
- Portfolios and/or Hybridized Algorithms within a Parallel Context
IMPORTANT DATES
Paper Submissions: ------------------------------------------- February 15, 2010
Acceptance Notification: ------------------------------------- March 15, 2010
Camera Ready Papers and Registration Due: -------------------- April 15, 2010
WORKSHOP ORGANIZERS
Michael Krajecki, CReSTIC, Universite de Reims Champagne-Ardennes, France
Email: michael.krajecki@univ-reims.fr
Lakhdar Sais, CRIL, Universite d'Artois, France
Email: sais@cril.univ-artois.fr
Gilles Dequen, MIS, Universite de Picardie, France
Email: gilles.dequen@u-picardie.fr
International Program Committee:
All submitted papers will be reviewed by the workshop technical program committee members following
similar criteria used in HPCS.
- Francois Bodin, IRISA, Rennes, France
- Clementin Tayou Djamegni, University of Dschang, Cameroon
- Youssef Hamadi, Microsoft Research Cambridge, U.K.
- Marijn Heule, TU Delft, The Netherlands
- Bertrand Le Cun, Universite de Versailles Saint-Quentin en Yvelines, France
- Tobias Schubert, Albert-Ludwigs-University of Freiburg, Germany
- Carsten Sinz, University of Karlsruhe, Germany
- Peter Stuckey, University of Melbourne, Australia
If you have any questions about paper submission or the workshop, please contact the Workshop
organizers at the above addresses.
|
| | | | |
| | |
| | |
| | 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.
|
| | | | |
| | |
| | |
| | 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 |
| | | | |
| | |
|  | |  | | | | | Date: | 11-May-2009 | | Title: | HLDVT 2009: Call for Papers
| | Hits: | 522 | | 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 |
| | | | |
| | |
| | | Call for Papers
CFV'09: Sixth International Workshop on Constraints in Formal
Verification
Grenoble, France, June 25, 2009.
A satellite event of the 21st International Conference on
Computer Aided Verification (CAV'09)
CFV'09 web site: http://www.miroslav-velev.com/cfv09.html
Abstract submission deadline: April 15
Paper submission deadline: April 22 |
| | | | |
| | |
| | | Call for Papers
CFV'09: Sixth International Workshop on Constraints in Formal
Verification
Grenoble, France, June 25, 2009.
A satellite event of the 21st International Conference on
Computer Aided Verification (CAV'09)
CFV'09 web site: http://www.miroslav-velev.com/cfv09.html
Abstract submission deadline: April 15
Paper submission deadline: April 22
Overview
---------------------------------------------
Formal verification is of crucial significance in the development of
hardware and software systems. In the last few years, tremendous
progress was made in both the speed and capacity of constraint
technology. Most notably, SAT solvers have become orders of magnitude
faster and capable of handling problems that are orders of magnitude
bigger, thus enabling the formal verification of more complex computer
systems. As a result, the formal verification of hardware and software
has become a promising area for research and industrial applications.
The main goals of the Constraints in Formal Verification workshop are
to bring together researchers from the CSP/SAT and the formal
verification communities, to describe new applications of constraint
technology to formal verification, to disseminate new challenging
problem instances, and to propose new dedicated algorithms for hard
formal verification problems.
This workshop will be of interest to researchers from both academia
and industry, working on constraints or on formal verification and
interested in the application of constraints to formal verification.
Scope
---------------------------------------------
The scope of the workshop includes topics related to the application
of constraint technology to formal verification, namely:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- challenging formal verification problems.
Delivery
---------------------------------------------
The workshop is scheduled for June 25, 2009. It will be
structured to allow ample time for discussion and demonstration of new
tools and new problem instances.
Submissions
---------------------------------------------
Submissions should be in the LNCS format and in one of the following types:
- a regular paper of up to 15 pages;
- a short paper of up to 4 pages, describing an industrial experience.
Workshop papers should be submitted electronically in pdf format.
Papers should be formatted using the Lecture Notes in Computer Science
(LNCS) style.
Paper submissions should be e-mailed to the workshop chairs at:
mvelev@gmail.com
Important Dates
---------------------------------------------
The important dates for the workshop are as follows:
- abstract submission deadline: April 15
- paper submission deadline: April 22
- notification of acceptance: May 10
- camera-ready version deadline: May 31
- workshop date: June 25
Invited Speakers
---------------------------------------------
Bernd Becker, University of Freiburg, Germany
Talk title: SAT and SMT Solving in a Multi-Core Environment
Workshop Chair
---------------------------------------------
Miroslav Velev, Aries Design Automation, U.S.A.
Masahiro Fujita, University of Tokyo, Japan
Program Committee
--------------------------------------------
Jay Bhadra, Freescale, U.S.A.
Sérgio Vale Aguiar Campos, Universidade Federal de Minas Gerais, Brazil
Maciej Ciesielski, University of Massachusetts, U.S.A.
Goerschwin Fey, University of Bremen, Germany
Alex D. Groce, NASA-JPL, U.S.A.
Michael Hsiao, Virginia Tech, U.S.A.
Chung-Yang (Ric) Huang, National Taiwan University, Taiwan
John Franco, University of Cincinnati, U.S.A.
Priyank Kalla, University of Utah, U.S.A.
Shin-ichi Minato, Hokkaido University, Japan
Steve Prestwich, University College Cork, Ireland
Andreas Veneris, University of Toronto, Canada |
| | | | |
| | |
| | | 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 |
| | | | |
| | |
| |
Journal on Satisfiability, Boolean Modeling and Computation
ISSN 1574-0617
Special Issue on Parallel SAT Solving
Call for Papers
Deadline for paper submission: November 30th, 2008
Guest Editor
Youssef Hamadi, Microsoft Research youssefh at microsoft dot com.
General Information
Recent years have shown a major architectural shift in computer hardware. The traditional efficiency
gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall
and performance improvements have to be found elsewhere. The new direction is to add more computing
units (cores) to a chip in order to raise its computational power. The products resulting from this
multi-core strategy are now on every desktop and yet the horizon is wide open since the number of
cores is expected to grow exponentially. This technological shift represents an important challenge
for many computer sciences fields whose best algorithms have to be rethought for multi-core-based
parallelization. The goal of this special issue is to officially acknowledge this evolution, and to
present recent advanced in the parallel processing of SAT problems.
Topics
We welcome the submission of works related to the parallel processing (shared-memory and/or
message-passing based) of SAT, MAX-SAT and QBF problems.
Submission
This special issue welcomes original high-quality contributions that have been neither published in
nor submitted to any journals. All submissions should be written in terms understandable by general
readers of the journal. All submissions will be refereed according to JSAT standards, as described
at JSAT web page. Submissions should be written in LaTeX and formatted with JSAT LaTeX style file
according to JSAT's author guidelines, and should not exceed 20 pages. Submissions should be emailed
to youssefh at microsoft dot com within the deadline marked above.
About JSAT
JSAT is a peer-reviewed journal which is freely distributed electronically and published in print by
IOS Press. The scope of JSAT is propositional reasoning, modeling and computation, and related
topics. JSAT publishes high-quality original research papers and survey papers which evidently
contribute to deeper insight on a SAT-related topic.
|
| | | | |
| | |
| | | Dear Colleague,
We would like to invite you to submit a paper to the special issue of
Annals of Mathematics and Artificial Intelligence (AMAI)
on the topic of application of Constraints to Formal Verification and AI (CFVAI).
The submission deadline is November 20, 2008.
Topics include, but are not limited to, the following:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- tuning SAT for formal verification and testing;
- scheduling, and planning;
- challenging formal verification, scheduling, and planning problems.
The submissions have to be in the AMAI format:
http://www.springer.com/computer/artificial/journal/10472
and have to be e-mailed to: mvelev@gmail.com
If possible, please email by October 10 to express your intent to submit a paper.
We look forward to your submission,
Miroslav Velev and John Franco
Editors of the special issue of AMAI on CFVAI |
| | | | |
| | |
| |
---
Last CFP Symcon'08
Submission deadline EXTENDED : Sunday, 6 July 2008
---
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
|
| | | | |
| | |
| |
* ______________________________________________________________________ *
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
|
| | | | |
| | |
| |
held in conjunction with CP'2008, Sydney, Australia, Sept 14, 2008.
Overview:
Constraint Programming is a very successful paradigm to express combinatoral
problems for which it provides both a representation language and powerful
solving techniques. Modeling uncertainty in data and/or the presence of an
adversary can be done by introducing universally quantified and/or stochastic
variables. They are used to encode possible alternative that have to be all
taken into account to provide a robust solution. Possible applications are
games, robust scheduling, conformant planning or model checking for the discrete
case. For continuous variables, it includes control design, verification of
safety and performance conditions of a system in engineering or determination of
values of design variables compatible with all values of some uncertain physical
data.
The first workshop on Quantification in Constraint Programming has been held in
conjuction with CP'2005 in Sitges, Spain. Since then, there has been an
increasing attention to this topic in the areas of QBF, QCSP and continuous
constraints. The aim of this workshop is to collect papers describing novel and
ongoing works in the field, and to foster discussions and cross-fertilization
between different approaches.
Scope:
This workshop is open to all aspects related to quantification in Constraint
Programming and SAT. The aim of the workshop is to present ongoing work and to
exchange ideas on modeling and solving quantified problems. Topics that may be
addressed in papers for consideration for inclusion in this workshop include,
but are not limited to:
- Search and propagation algorithm
- Modeling issues with quantified languages
- Complexity results
- Quantified global constraints
- Quantified languages design and compilation
- Strategy extraction and representation
- Over-constrained quantified problems, explanations
- First-order constraints
- Quantification in CHR
- Uncertainty handling
- Stochastic constraint programming
- Implementation issues
- Other types of variables, non-backtrackable variables where domain prunings are not undone
on backtracking
- Applications and benchmarks of Quantified Constraints, QBF and Stochastic CSP
Submissions:
The workshop is open to all members of the CP community. Submitted papers can
be up to 15 pages in length, describing work on one or more of the topics
relevant to the workshop. Alternatively, a shorter paper (maximum 5 pages) can
be submitted, presenting a research statement or perspective on topics relevant
to the workshop. All submissions will be reviewed and accepted papers will be
published in the workshop proceedings. At least one author must attend the
workshop. The proceedings will be available electronically on the workshop web
page and in hardcopy at CP 2008.
We encourage authors to submit papers electronically in pdf format. Papers
should be formatted using the Lecture Notes in Computer Science (LNCS) style.
All submissions should include the author's name(s), affiliation, complete
mailing address, and email address. Workshop papers will be published in
workshop notes as well as on the Web.
Please send your submission by email to the workshop organizers,
using the subject line "QiCP'2008 submission": enrico@dist.unige.it, arnaud.lallouet@univ-orleans.fr, rueher@essi.fr
Important Dates:
Paper submission : July 11, 2008
Notification : July 30, 2008
Final version : August 20, 2008
Organizing Committee:
Enrico Giunchiglia, University of Genova, Italy.
Arnaud Lallouet, University of Orléans, France.
Michel Rueher, University of Nice, France.
|
| | | | |
| | |
| | | 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 |
| | | | |
| | |
| | | | | | | | Date: | 14-Apr-2008 | | Title: | CFV'08 --- Fifth International Workshop on Constraints in Formal Verification
| | Hits: | 838 | | Contributed by: | Miroslav Velev | | Keywords: | Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, Satisfiable Problems Generation, SAT tools, CSP, Logic, branching heuristics, call for papers |
| | | | | | |
| | | Call for Papers:
CFV'08 --- Fifth International Workshop on Constraints in Formal Verification,
a satellite event of IJCAR'08.
Invited are papers on application of SAT to formal verification and constraint solving.
Abstract submission deadline: May 15.
Paper submission deadline: May 22.
Workshop dates: August 10-11, 2008.
Location: Sydney, Australia. |
| | | | |
| | |
| | |
BPR 2008
First International Workshop on Bit-Precise Reasoning
Princeton, New Jersey. July 14th, 2008
Call for Papers
http://www.cs.ubc.ca/~babic/index_bpr.htm
Important Dates
* Submission: April 28th, 2008
* Notification: June 2nd, 2008
* Final version: June 9th, 2008
* Workshop: July 14th, 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
|
| | | | |
| | |
| |
SAT 2008
Call for Papers
11th International Conference on
Theory and Applications of Satisfiability Testing
May 12 - 15, Guangzhou, P. R. China
http://www.upb.de/cs/SAT08
The International Conference on Theory and Applications of
Satisfiability Testing is the primary annual meeting for researchers
studying the propositional satisfiability problem (SAT). SAT08 is
the eleventh SAT conference. SAT08 features the SAT Race, the
Max-SAT Evaluation, and the QBFEVAL.
SCOPE
Many hard combinatorial problems can be encoded into SAT.
Therefore improvements on heuristics on the practical side, 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/SAT2008. Papers have to be submitted
electronically as PDF files.
IMPORTANT DATES
January 11, 2008 Abstract Submission
January 18, 2008 Paper Submission
February 18, 2008 Author Notification
February 25, 2008 Final Version
PROGRAM CHAIRS
Hans Kleine Büning, University of Paderborn, Germany
Xishun Zhao, Sun Yat-Sen University, Guangzhou, P.R. China
LOCAL CHAIR / Organization Committee
Shier Ju, Sun Yat-Sen University, Guangzhou, P.R. China
Minghui Xiong, Sun Yat-Sen University, Guangzhou, P.R. China
Lin Xu, Natural Science Foundation of China, P.R. China
Uwe Bubeck, University of Paderborn, Germany
Theo Lettmann, University of Paderborn, Germany
SAT Race
Carsten Sinz, Universität Tübingen, Germany
et al.
QBFEVAL
Massimo Narizzano, Università di Genova, Italy
Luca Pulina, Università di Genova, Italy
Armando Tacchella, Università di Genova, Italy
Max-SAT EVALUATION
Josep Argelich, Universitat de Lleida, Spain
Chu Min Li, Université de Picardie, France
Felip Manya, Universitat de Lleida, Spain
Jordi Planes, University of Southampton, UK
Further information on SAT Race, Max-SAT Evaluation, and QBFEVAL
will be published also on the SAT08 conference web page.
|
| | | | |
| | |
| | EPIA 2007
13th Portuguese Conference on Artificial Intelligence
** Workshop on Search Techniques for Constraint Satisfaction **
http://epia2007.appia.pt/stcs
Call for Papers
December 3-7, Guimaraes, Portugal
Search is essential for solving combinatorial problems in AI. For the usual
case where inference based methods are incomplete, search provides the core
engine for applications such as hardware verification, planning, or protein
folding.
Recent advances in Constraint Programming (CP) and Boolean algorithms for
Propositional Satisfiability (SAT), Pseudo-Boolean Optimization (PBO),
Satisfiability-Modulo Theories (SMT) and Quantified Boolean Formulas (QBF)
have allowed current solvers to perform several orders of magnitude faster
than previous ones. This workshop aims at bringing together researchers and
practitioners from these communities, in order to learn from each other,
develop common understandings, and inspire new applications, algorithms and
approaches.
TOPICS OF INTEREST
The topics of the workshop span practical and theoretical research on search
techniques for constraint satisfaction and include but are not limited to:
Complete and local search algorithms
Analysis of search algorithms
Search heuristics
Search space pruning techniques
Problem encodings for combinatorial problems using constraint programming
and propositional satisfiability
Novel applications using constraint satisfaction components
Implementation techniques for constraint satisfaction and combinatorial
optimization search algorithms
Distributed and parallel algorithms for constraint satisfaction
Case studies and empirical results
SUBMISSION
Authors should submit full papers with a maximum of 12 pages using Springer
LNCS format. Submission is double blind. A selection of the workshop accepted
full papers will be published by Springer LNAI sub-series. All the other
accepted papers will be published in the workshop proceedings.
IMPORTANT DATES
Submission Deadline: 30.June.2007
Notification of acceptance: 28.July.2007
Workshop and EPIA 2007: 3-7.December.2007
ORGANISING COMMITTEE
Francisco Azevedo, New University of Lisbon, Portugal
Ines Lynce, Technical University of Lisbon, Portugal
Vasco Manquinho, Technical University of Lisbon, Portugal
PROGRAM COMMITTEE
Pedro Barahona, Universidade Nova de Lisboa, Portugal
Lucas Bordeaux, Microsoft Research, UK
Carla Gomes, Cornell University, USA
Zeynep Kiziltan, Università di Bologna, Italy
Oliver Kullmann, University of Wales Swansea, UK
Daniel Le Berre, Université d'Artois, France
Felip Manyà, Universitat de Lleida, Spain
João Marques-Silva, University of Southampton, UK
Pedro Meseguer, IIIA-CSIC Barcelona, Spain
Steven Prestwich, University College Cork, Ireland
Olivier Roussel, Université d'Artois, France
Carsten Sinz, University of Tübingen, Germany
Barbara Smith, Cork Constraint Computation Centre, Ireland
Armando Tachella, Università di Genova, Italy
Mark Wallace, Monash University, Australia
|
| | | | |
| | |
| | [Apologies for multiple copies]
http://research.microsoft.com/constraint-reasoning/Workshops/Autonomous-CP07/default.htm
First Workshop on Autonomous Search
In conjunction with CP’2007. September 23, 2007, Providence, Rhode Island, USA
Workshop description
Recent progresses in the processing of combinatorial problems have demonstrated
that search algorithms can become extremely efficient when they take advantage
of unsuccessful attempts to drive their exploration. For instance in modern
DPLLs, the collect of conflicts feeds the variable selection heuristic, and the
quality of unit propagation controls the use of the restart strategy. These
implicit uses of closed control loops have been empirically discovered by the
SAT community.
We believe that a more principled and autonomous approach for search efficiency
has to be started in Constraint Programming. This first workshop will promote
works interested in the dynamic and autonomous adaptation of search procedures.
The meeting will not particularly focus on the presentation of state of the art
search results, but favour works demonstrating the premises of effective
self-adaptation.
In order to encourage the systematic and principled exploration of autonomous
search, this event will welcome works on all the aspects of self-improving
combinatorial search. Typical topics include, but are not limited to:
· Adaptive/Reactive search
· Self configuration of search
· Self optimization of search
· Meta-search
· Self-hybridizing search
· Learning for search
· Explanations analysis
· Impact-based heuristics
Workshop proceedings
To come.
Schedule
To come.
Attendance
At least one author of each accepted submission must attend the workshop.
Presentation and submission format
Half-day workshop. Full papers of no more than 15 pages formatted using the
LNCS style, http://www.springer.de/comp/lncs/authors.html. Short papers (at
least 3 pages or 3,000 words) addressing an important problem for further
research or describing an interesting lesson learned. Papers must be addressed
in pdf to youssefh at microsoft dot com.
Important dates
Submission deadline: June 29th
Notification of acceptance: July 21th
Camera-ready copy deadline: August 1st
CP workshops: September 23th
CP conference: September 23th-27th
Program committee
· Lucas Bordeaux, MSR, UK
· Roberto Battiti, U. of Trento, Italy
· Chris Beck, U. of Toronto, Canada
· Carlos Castro, UTFSM, Chile
· Susan L. Epstein, Hunter College and The Graduate Center/CUNY, USA
· Youssef Hamadi, MSR, UK
· Rashidi Haramabadi, U. of Essex, UK
· Jin-Kao Hao, U. d’Angers, France
· Michail G. Lagoudakis, Technical U. of Crete, Greece
· Eric Monfroy, UTFSM, Chile and U. of Nantes, France
· Jacques Pitrat, CNRS/U. Pierre et Marie Curie, France
· Philippe Refalo, Ilog, France
· Frederic Saubion, U. d’Angers, France
· Horst Samulowitz, U. of Toronto, Canada
· Marc Schoenauer, INRIA Futurs, France
Contact information
Youssef Hamadi, Microsoft Research, Cambridge, UK. Email: youssefh at microsoft
dot com
Eric Monfroy, Université de Nantes, France. Email: Eric dot Monfroy at lina dot
univ-nantes dot fr
Frederic Saubion, Université d’Angers, France. Email: Frederic dot Saubion at
univ-angers dot fr |
| | | | |
| | |
| | | Call for Papers
CFV'07: Fourth International Workshop on Constraints in Formal Verification
Bremen, Germany, July 16, 2007
A satellite event of the 21st Conference on Automated Deduction (CADE-21)
CFV'07 web site: http://www.miroslav-velev.com/cfv07.html
Submission deadline: May 15, 2007
Scope:
The scope of the workshop includes topics related to the application
of constraint technology to formal verification, namely:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- challenging formal verification problems. |
| | | | |
| | |
| | | | | | | | Date: | 05-Apr-2007 | | Title: | CFV'07 Call for Papers
| | Hits: | 1451 | | Contributed by: | Miroslav Velev | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Local Search, BDD, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Instance simplification, Learning, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, QBF, Dynamic restarts, variable ordering heuristic, preprocessors, call for papers, conference information, Boolean functions, Linear Constraints, SAT Hardware, Satisfiability Modulo Theory, Constraint Programming, SAT/CP |
| | | | | | |
| | | The Fourth Workshop on Constraints in Formal Verification will take place in Bremen, Germany, on July 16, 2007, as a satellite event of CADE-21.
The submission deadline is May 15, 2007:
http://www.miroslav-velev.com/cfv07.html |
| | | | |
| | |
| |
* ________________________________________________________________ *
The RCRA group (Knowledge Representation & Automated Reasoning) of the
AI*IA (Italian Association for Artificial Intelligence) organises the
14th RCRA workshop:
Experimental evaluation of algorithms for solving problems
with combinatorial explosion
http://pst.istc.cnr.it/RCRA07/
rcra07@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.
* ________________________________________________________________ *
DATE
5-6 July 2007
VENUE
Rome, CNR (National Research Council)
AIMS AND SCOPE
Many problems in Artificial Intelligence show an exponential explosion
of the search space. Although stemming from different research areas
in AI, such problems are often addressed with algorithms that have
a common goal: the effective exploration of huge state spaces. Many algorithms
developed in one research area are applicable to other problems, or can be
hybridised with techniques in other areas. Artificial Intelligence tools
often exploit or hybridise techniques developed by other research communities,
such as Operations Research.
In recent years, research in AI has more and more focussed on experimental
evaluation of algorithms, the development of suitable methodologies for
experimentation and analysis, the study of languages and the implementation
of systems for the definition and solution of problems.
Scope of the workshop is fostering the cross-fertilisation of ideas
stemming from different areas, proposing benchmarks for new challenging
problems, comparing models and algorithms from an experimental viewpoint,
and, in general, comparing different approaches with respect to efficiency,
problem modelling, and ease of development.
[...]
Publications showing negative results are welcome, provided that the
approach was original and very promising in principle, the experimentation
was well-conducted, the results obtained were unforeseeable and gave
important hints in the comprehension of the target problem, helping
other researchers to avoid unsuccessful paths.
WORKSHOP CHAIRS
* Marco Gavanelli, Università degli Studi di Ferrara
* Toni Mancini, Università di Roma "La Sapienza"
LOCAL COMMITTEE
* Amedeo Cesta, ISTC-CNR, Rome
* Nicola Policella, ISTC-CNR, Rome
IMPORTANT DATES
* Paper submission deadline: 25 April 2007
* Notification of acceptance/reject: 25 May 2007
* Final version: 20 June 2007
* Workshop: 5-6 July 2007
SUBMISSIONS
Papers should not exceed 15 pages (Latex standard article style, 11pt) and
should be submitted electronically via email to rcra07@dis.uniroma1.it, either
in postscript or PDF format.
Two types of submissions are possible
* Original papers, not previously published in conferences or journals
* Informal presentations, overviews of research projects, position papers
Both types of submissions will be reviewed by at least three members of the program committee.
Accepted papers will be electronically published on the workshop web site.
Informal presentations are aimed at fostering discussion between the participants.
After the workshop, the authors of original papers will be invited to submit an extended
version of their paper for possible publication in the post-proceedings.
|
| | | | |
| | |
| |
Engineering Stochastic Local Search Algorithms
---
Designing, Implementing and Analyzing Effective Heuristics
SLS 2007
6-8 September, 2007. Brussels, Belgium
More details and up-to-date information at
www.stochastic-local-search.net/sls07
Scope of the Workshop
======================
Stochastic local search (SLS) algorithms are among the most powerful
techniques for solving computationally hard problems in many areas
of computer science, operations research and engineering. SLS
techniques range from rather simple constructive and iterative
improvement algorithms to general-purpose methods, also widely known
as metaheuristics, such as ant colony optimization, evolutionary
computation, iterated local search, memetic algorithms, simulated
annealing, tabu search and variable neighbourhood search.
In recent years, it has become evident that the development of
effective SLS algorithms is a highly complex engineering process
that typically combines aspects of algorithm design and
implementation with empirical analysis and problem-specific
background knowledge. The difficulty of this process is due in part
to the complexity of the problems being tackled, and in part to the
large number of degrees of freedom researchers and practitioners
face when developing SLS algorithms.
This development process needs to be assisted by a sound methodology
that adresses the issues arising in the phases of algorithm design,
implementation, tuning and experimental evaluation. In addition,
more research is required to understand which SLS techniques are
best suited for particular problem types and to better understand
the relationship between algorithm components, parameter settings,
problem characteristics and performance.
Publication
============
The workshop proceedings will be published in Springer's Lecture
Notes in Computer Science (LNCS) series.
Important Dates
================
Extended Submission deadline 8 April, 2007
Notification of acceptance 21 May, 2007
Camera ready copy 4 June, 2007
Workshop 6-8 September, 2007
Further Information
====================
Up-to-date information will be published on the web site
www.stochastic-local-search.net/sls07. For information about local
arrangements, registration forms, etc., please refer to the
above-mentioned web site or contact the local organizers.
SLS 2007 Workshop Committee
============================
General Chairs
Thomas Stuetzle, IRIDIA, CoDE, ULB, Brussels, Belgium
Mauro Birattari, IRIDIA, CoDE, ULB, Brussels, Belgium
Holger H. Hoos, CS Department, UBC, Vancouver, Canada
|
| | | | |
| | |
| | | SAT researchers who would like to present their work to the broad AI community may be interested in the following call for papers. It asks for short reports on important work that has already appeared at specialized or non-AI events, such as SAT.
Call for Papers
AAAI-07 Nectar Track
July 22-26, 2007
Vancouver, British Columbia, Canada
AAAI-07 will again include the Nectar track, whose goal is
to make the most significant AI results presented in sister
conferences in the last two years available to a broad AI
audience.
The Nectar (new scientific and technical advances in
research) track will consist of papers that are based on
important results that have already been published in the
proceedings of at least one major specialized conference in
2005 and 2006, as either a single paper or a series of
papers. Examples of such conferences include AAMAS, AIIDE,
ALIFE, ACL, CEC, CogSci, CP, FUZZ-IEEE, GECCO, ICAPS, ICCBR,
ICML, ICRA, IEEE CEC, IJCNN, IROS, ISWC, IUI, KCAP, KR,
NIPS, RSS, SAT, UAI and WCCI. Examples of conferences in
related fields with relevance to AI are ALife, CIKM, COLT,
KDD, PODS, ICDTSIGIR, SIGMOD, VLDB, and WWW. Papers that
report on the application of AI techniques in other fields,
for example bioinformatics, may also serve as the basis for
Nectar papers. Authors of application papers, however, are
advised that they may find the conference on innovative
applications of AI (IAAI) a more appropriate venue for
reaching the AI community since those papers can be longer
and thus provide a clearer application setting in which to
describe the work. Papers that have appeared in either AAAI
or IJCAI cannot serve as the basis for Nectar papers since
they have already been presented to the entire AI community.
One important goal of the track is to offer young
researchers the opportunity to learn about areas with which
they may not already be familiar. Another goal is to
encourage the sort of cross-disciplinary AI work that has
historically been supported by AAAI.
We solicit short submissions of up to four pages. Each
submission should focus on a major result that has already
been published in one or more venues as described above. A
Nectar paper needs to clarify the relationship of the paper
to any other AAAI-07 submissions by the authors and cannot
overlap with them substantially. The Nectar paper should
cite the previous publication(s) and will typically devote
no more than one or two pages to summarizing the core
results. The remainder of the paper should be devoted to
putting the results, as well as the problem they solve, into
a context that is meaningful to a wide AI audience.
AAAI Nectar track papers will be presented as short talks or
posters at AAAI-07. The papers will also be published in the
conference proceedings. Submitted papers will be reviewed
according to: (1) significance of the result to the broad
goals of AI, (2) potential for the result to influence work
in other areas of AI, and (3) clarity of the presentation to
a wide AI audience.
Although papers will describe previously published results,
the paper itself must be original. Authors of accepted
papers will be required to transfer copyright.
Papers must be received by February 27, 2007. Decisions on
the acceptance of papers will be made by March 29, 2007.
For more information, as it becomes available, please see
www.aaai.org/Conferences/AAAI/aaai07.php and
www.aaai.org/Conferences/AAAI/2007/aaai07nectarcall.php
Elaine Rich (University of Texas at Austin), Cochair
Sven Koenig (University of Southern California), Cochair |
| | | | |
| | |
| | | | | | | | Date: | 26-Nov-2006 | | Title: | Special issue of JSAT on CFV
| | Hits: | 2059 | | Contributed by: | Miroslav Velev | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, MAC, FC, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, Cellular Automata, Cellection Framework, call for papers, semidefinite programming, conference information, Genetic Algorithm, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware, Lookahead, Generative SAT library, multi-value, Stochastic Satisfiability, Divide-and-Conquer Algorithms, Non-monotonic reasoning, implicativity, stable set of points, stable set of clusters, Satisfiability Modulo Theory, Constraint Programming, genetic programming, SAT/CP, bioinformatics, resolution determinization, SAT-solver, SAT/CP Integration, Hybrid solver, Visualisation, Pseudo-Boolean Solving, Resolution proof |
| | | | | | |
| | | Dear Colleague,
We would like to invite you to submit a paper to the special issue of the
Journal on Satisfiability, Boolean Modeling and Computation (JSAT) on
the topic of application of constraints to formal verification (CFV).
The submission deadline is January 10, 2007.
Topics include, but are not limited to, the following:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- tuning SAT for formal verification and testing;
- challenging formal verification problems.
The submissions have to be in the JSAT format:
http://www.isa.ewi.tudelft.nl/Jsat/
and have to be e-mailed to: mvelev@gmail.com
If possible, please confirm your intent to submit a paper.
We look forward to your submission,
Miroslav Velev and Joao Marques-Silva
Editors of the special issue of JSAT on CFV |
| | | | |
| | |
| | | | | | | | Date: | 21-Oct-2006 | | Title: | special track on 'applied formal verification' of EuroCAST'07
| | Hits: | 1479 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, Local Search, Computational logic, Verification, Alternative approach, QBF, EDA, SAT application, SAT tools, MAXSAT, call for papers, SAT-Based, Satisfiability Modulo Theory, Constraint Programming |
| | | | | | |
| |
special track on 'applied formal verification' of EuroCAST'07 on the
Canarian Islands.
The Workshop concentrates on formal verification engines and to improve
practicability and scalability of formal methods. Topics include, but
not exclusively, the following: Satisfiability (SAT); Satisfiability
Modulo Theories (SMT); Quantified Boolean Formulas (QBF); Constraint
Programming (CP); Equivalence Checking (EC); Model Checking (MC);
Theorem Proving (TP). Case studies and papers in the border line of
verification, including synthesis, compilation and modelling, are also
welcome
Important dates:
- Extended Abstract, 2 pages, deadline 31. October
- Decision 1. December
- Workshop 12.-16. February 2007.
- Full Papers Post-Conference LNCS Volume, 31. April 2007.
|
| | | | |
| | |
| | | | | | | | Date: | 12-Oct-2006 | | Title: | SAT 2007 Call For Paper: deadline for submission is January 19, 2007
| | Hits: | 1495 | | 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 PAPERS: TACAS 2007
Thirteenth International Conference on
Tools and Algorithms for the Construction and Analysis of Systems
www.doc.ic.ac.uk/tacas07/
Part of ETAPS 2007, March 24 - April 1, 2007, Braga, Portugal
IMPORTANT DATES
---------------
* 6 Oct 2006: Submission deadline (strict) for abstracts of research and
tool demonstration papers
* 13 Oct 2006: Submission deadline (strict) for full versions of
research and tool demonstration papers
* 8 Dec 2006: Notification of acceptance
* 5 Jan 2007: Camera-ready versions due
CONFERENCE DESCRIPTION
----------------------
TACAS is a forum for researchers, developers and users interested in
rigorously based tools and algorithms for the construction and analysis
of systems. The conference serves to bridge the gaps between different
communities that share common interests in, and techniques for, tool
development and its algorithmic foundations. The research areas covered
by such communities include but are not limited to formal methods,
software and hardware verification, static analysis, programming
languages, software engineering, real-time systems, communications
protocols, and biological systems. The TACAS forum provides a venue for
such communities at which common problems, heuristics, algorithms, data
structures and methodologies can be discussed and explored. In doing so,
TACAS aims to support researchers in their quest to improve the utility,
reliability, flexibility and efficiency of tools and algorithms for
building systems.
Tool descriptions and case studies with a conceptual message, as well
as theoretical papers with clear relevance for tool construction are all
encouraged. The specific topics covered by the conference include, but
are not limited to, the following:
* Specification and verification techniques for finite and
infinite-state systems
* Software and hardware verification
* Theorem-proving and model-checking
* System construction and transformation techniques
* Static and run-time analysis
* Abstraction techniques for modeling and validation
* Compositional and refinement-based methodologies
* Testing and test-case generation
* Analytical techniques for secure, real-time, hybrid, critical,
biological or dependable systems
* Integration of formal methods and static analysis in high-level
hardware design or software environments
* Tool environments and tool architectures
* SAT solvers
* Applications and case studies
As TACAS addresses a heterogeneous audience, potential authors are
strongly encouraged to write about their ideas and findings in general
and jargon-independent, rather than in application- and domain-specific,
terms. Authors reporting on tools or case studies are strongly
encouraged to indicate how their experimental results can be reproduced
and confirmed independently.
|
| | | | |
| | |
| | | | | | | | Date: | 09-May-2006 | | Title: | Fourth International Workshop on Constraints in Formal Verification (CFV'06)
| | Hits: | 1876 | | Contributed by: | Miroslav Velev | | Keywords: | Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware |
| | | | | | |
| | | Fourth International Workshop on
Constraints in Formal Verification.
Affiliated with
International Joint Conference on Automated Reasoning
2006 Federated Logic Conference,
Seattle, U.S.A., August 22, 2006.
The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems.
This workshop will be of interest to researchers from academia and industry, working in constraints or in formal verification and interested in the application of constraints in formal verification.
The scope of the workshop includes topics related with the application of constraint technology in formal verification, namely:
-application of constraint solvers to hardware verification;
-application of constraint solvers to software verification;
-dedicated solvers for formal verification problems;
-challenging formal verification problems.
Submissions can include one of the following:
-A workshop paper of up to 15 pages in LNCS format;
-A short paper of up to 4 pages, in LNCS format, describing an industrial experience.
Important Dates:
-Paper submission deadline June 5th;
-Notification of acceptance July 5th;
-Camera-ready version deadline July 20th;
-Workshop Date August 22nd. |
| | | | |
| | |
| | | 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 |
| | | | |
| | |
| | | Papers on all aspects of SAT and formal verification are invited for submission to the 3rd International Workshop on Constraints in Formal Verification, Tallinn, Estonia, July 23, 2005, to be held in conjunction with CADE-20.
The submission deadline was extended till June 15. |
| | | | |
| | |
| | | Submission deadline approaching: 9 April 2005 |
| | | | |
| | |
| | | The deadline for CHARME'05 (Correct Hardware Design and Verification Methods)
has been extended to April 8, 2005. Abstracts are still due on March 29, 2005.
For details, see http://www.charme2005.com |
| | | | |
| | |
| | | The 3rd International Workshop on Constraints in Formal Verification (CFV), associated with the 20th International Conference on Automated Deduction (CADE-20), will be held on July 23, 2005, in Tallinn, Estonia, and has a submission deadline of June 5.
Papers on applying SAT/CSP to formal verification are welcome. |
| | | | |
| | |
| | | SAT papers are invited for submission to CHARME '05: 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Saarbrücken, Germany, October 2005. |
| | | | |
| | |
| | | Papers on all SAT topics are invited.
The related track is:
6. Computer-Aided Network Design,
and possible subtracks:
6.6: Advances in Formal Verification;
6.7: Fundamentals of CAD Algorithms;
6.11: Other Areas in CAD.
The submission deadline is October 8, 2004. |
| | | | |
| | |
| | | SAT is one of the topics in Track 1, AI.
The submission deadline is September 3, 2004. |
| | | | |
| | |
| | | SAT is one of the topics.
The deadline is July 5, but submissions that are up to 1 week late will be reviewed. |
| | | | |
| | |
| | | Authors are invited to submit papers on SAT and formal verification topics to Microprocessor Test and Verification (MTV '05), to take place September 9-10, 2004, in Austin, Texas, USA.
The submission deadline is May 31, 2004. |
| | | | |
| | |
| | SAT 2005
Special issue of the Journal of Automated Reasoning
Guest Editors: Enrico Giunchiglia and Toby Walsh
In the last ten years, much progress has been made in our ability to
solve problems in propositional satisfiability (or SAT) and related
areas. In 2000, a very successful special issue of the Journal of
Automated Reasoning and an accompanying book documented the progress
made up to that time. In the subsequent five years, even more dramatic
progress has been made. Systematic methods can now routinely solve
verification problems with thousands or tens of thousanss of variables,
whilst local search methods can solve hard random 3SAT problems with
millions of variables. In light of this, we are planning another special
issue of the Journal of Automated Reasoning, SAT 2005, on the state of
the art for research into satisfiability in the year 2005. In addition
to the special issue, the accepted papers will be published as a book
which will be included as an optional extra in the registration package
for the SAT-2005 conference. |
| | | | |
| | |
| | | Papers are invited to special sessions on SAT at Microprocessor Test and Verification (MTV'04), to take place in Austin, Texas, at the end of May. The approximate submission deadline is March 31. |
| | | | |
| | |
| | | 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 |
| | | | |
| | |
| | | Papers are invited to special sessions on SAT at Microprocessor Test and Verification (MTV'04), to take place in Austin, Texas, at the end of May.
The approximate submission deadline is March 15.
(More details later.) |
| | | | |
| | |
© 2000-2001 Business & Technology Research Laboratory.
© 2001-2005 Centre de Recherche en Informatique de Lens.
Hosted by Innovation
and Technology Research Lab.
Please send any comment to daniel@satlive.org.
|
|
|
