Joint Workshop on
Implementation of Constraint Logic Programming Systems
Logic-based Methods in Programming Environments
Satellite event of ICLP 2010
Edinburgh, Scotland, U.K.
July 15, 2010
CICLOPS is a series of colloquia on the implementation of constraint logic programming. Logic and Constraint programming is an important declarative programming paradigm. The features offered by this paradigm such as rule-basedness, pattern matching, automated backtracking, recursion, tabling, and constraint solving have been proved convenient for many programming tasks. Recent improvements in implementation technologies combined with advances in hardware and systems software have made logic and constraint programming a viable choice for many real-world problems.
CICLOPS'10 continues a tradition of successful workshops on Implementations of Logic Programming Systems, previously held with in Budapest (1993) and Ithaca (1994), the Compulog Net workshops on Parallelism and Implementation Technologies held in Madrid (1993 and 1994), Utrecht (1995) and Bonn (1996), the Workshop on Parallelism and Implementation Technology for (Constraint) Logic Programming Languages held in Port Jefferson (1997), Manchester (1998), Las Cruces (1999), and London (2000), and more recently the Colloquium on Implementation of Constraint and LOgic Programming Systems in Paphos (Cyprus, 2001), Copenhagen (2002), Mumbai (2003), Saint Malo (France, 2004), Sitges (Spain, 2005), Seattle (U.S.A., 2006), Porto (Portugal, 2007), Udine (Italy, 2008), and Pasadena (U.S.A, 2009).
WLPE is a series of workshops on practical logic-based software development methods and tools. Software plays a crucial role in modern society. While software keeps on growing in size and complexity, it is more than ever required to be delivered on time, free of error and meeting the most stringent efficiency requirements. Thus more demands are placed on the software developer, and consequently, the need for methods and tools that support the programmer in every aspect of the software development process is widely recognized. Logic plays a fundamental role in analysis, verification and optimization in all programming languages, not only in those based directly on logic. The use of logic-based techniques in software development is a very active area in computing; emerging programming paradigms and growing complexity of the properties to be verified pose new challenges for the community, while emerging reasoning techniques can be exploited.
WLPE'10 continues the series of successful international workshops on logic programming environments held in Ohio, USA (1989), Eilat, Israel (1990), Paris, France (1991), Washington D.C., USA (1992), Vancouver, Canada (1993), Santa Margherita Ligure, Italy (1994), Portland, USA (1995), Leuven, Belgium (1997), Las Cruces, USA (1999), Paphos, Cyprus (2001), Copenhagen, Denmark (2002), Mumbai, India (2003), Saint Malo, France (2004), Sitges (Barcelona), Spain (2005), Seattle, USA (2006), Porto, Portugal (2007) and Udine, Italy (2008). More information about the series of WLPE workshops can be found at http://www.cs.usask.ca/projects/envlop/WLPE/
CICLOPS-WLPE 2010 aims at bringing together, in an informal setting, people involved in research in the design and implementation of logic and constraint programming languages and systems and on logic-based methods and tools which support program development and analysis. In addition to papers describing more conceptual and theoretical work, papers describing the implementation of, and experience with, such tools will be welcome.
Topics include, but are not limited to:
- Abstract machines and compilation techniques
- Compile-time analysis and its application to code generation
- Memory management, indexing, and garbage collection issues
- Profiling tools and performance evaluation
- Implementation of concurrent, parallel, and distributed systems
- Extensions such as tabling, constraints, probabilistic reasoning, and learning
- New features such as ASP and coinduction
- Object-oriented and module systems
- Integration with other systems such as CP, SAT, LP/MLP, and Database systems
- Experiences from using systems in real-life applications
- Static and dynamic analysis
- Debugging and testing
- Program verification and validation,
- Code generation from specifications,
- Termination analysis,
- Profiling and performance analysis,
- Type and mode analysis,
- Module systems,
- Optimization tools,
- Program understanding,
- Logical meta-languages
|Paper Submission:||March 31, 2010|
|Notification of Authors:||April 29, 2010|
|Camera-ready:||May 17, 2010|
|Conference:||July 15, 2010|
Michael Codish, Ben-Gurion University of the Negev (Israel)
Programming with Boolean SatisfactionIn recent years, research on Boolean satisfiability (SAT) is generating remarkably powerful SAT solvers capable of handling larger and larger SAT instances. With the availability of progressively stronger SAT solvers, an accumulating number of applications have been developed which demonstrate that real world problems can often be solved by encoding them into SAT. One of the success stories is the application to termination analysis where we aim to automatically provide proofs of termination for software. Here, in the past five years, Boolean satisfiability has completely revolutionized the field.
One major obstacle in applying SAT solving to a given problem is to devise a suitable representation of the problem. This involves mapping the problem to a propositional formula in such a way that a model of the formula represents a solution of the original problem. This activity is just like programming (with logic): variables are Booleans and programs are formulas in conjunctive normal form. With expertise in declarative, logic and constraint programming, our community is well situated to join efforts in the development of new SAT encoding techniques and new applications for SAT solving. In this talk I will survey several SAT encoding techniques which come up in the application to termination analysis as well as in other applications.
Naoyuki Tamura, Kobe University (Japan)
Solving Constraint Satisfaction Problems by a SAT Solver
A Boolean Satisfiability Testing Problem (SAT) is a combinatorial
problem to find a Boolean variable assignment which satisfies all
given Boolean formulas. Recent performance improvement of SAT
technologies makes SAT-based approaches applicable for solving hard
and practical combinatorial problems, such as planning, scheduling,
hardware/software verification, and constraint satisfaction,
(joint work with Tomoya Tanjo and Mutsunori Banbara,
Kobe University, Japan)
Sugar is a SAT-based constraint solver based on a new encoding method called order encoding which was first used to encode job-shop scheduling problems by Crawford and Baker. In the order encoding, a comparison x<=a is encoded by a different Boolean variable for each integer variable x and integer value a. The Sugar solver shows a good performance for a wide variety of problems, and became the winner of the GLOBAL categories in 2008 and 2009 CSP solver competitions.
The talk will provide an introduction to modern SAT solvers, SAT encodings, implementation techniques of the Sugar solver, and its performance evaluation.
|Rafael Caballero||Complutense University Madrid, Spain|
|Vitor Santos Costa||Universidade do Porto, Portugal|
|Martin Gebser||University of Potsdam, Germany|
|Samir Genaim||Complutense University of Madrid, Spain|
|Yoshitaka Kameya||Tokyo Institute of Technology, Japan|
|Andy King||University of Kent, UK|
|Huiqing Li||University of Kent, U.K.|
|Lunjin Lu||Oakland University, MI, USA|
|Paulo Moura||Universidade da Beira Interior, Portugal|
|Ulrich Neumerkel||Technische Universit¨t Wien, Austria|
|Enrico Pontelli||New Mexico State University, USA|
|Joachim Schimpf||Monash University, Australia|
|Peter Schneider-Kamp||University of Southern Denmark, Denmark|
|Wim Vanhoof||University of Namur, Belgium|
|German Vidal (co-chair)||Technical University of Valencia|
|Neng-Fa Zhou (co-chair)||The City University of New York, NY, USA|
Informal proceedings will be published as a technical report and distributed at the workshop, as well as electronically at the Computing Research Repository (CoRR).
All papers must describe original, previously unpublished research, and must not simultaneously be submitted for publication elsewhere. They must be written in English. Papers must not exceed 15 pages in the Springer LNCS format.
Papers should follow the Springer LNCS format and be submitted electronically at http://www.easychair.org/conferences/?conf=ciclopswlpe2010
09:00‑10:00 Invited Talk (Chair: Neng-Fa Zhou)
Naoyuki Tamura (Kobe University, Japan)
Solving Constraint Satisfaction Problems by a SAT Solver
10:30‑12:30 Session 2
Peter Biener, François Degrave and Wim Vanhoof
A Test Automation Framework for Mercury
Realizing evaluation strategies by hierarchical graph rewriting
Nicos Angelopoulos and Paul Taylor
An extensible web interface for databases and its application to storing biochemical data
14:00‑15:00 Invited talk(Chair: German Vidal)
- Michael Codish (Ben-Gurion University of the Negev, Israel)
Programming with Boolean Satisfaction
15:30‑18:00 Session 4
Jan Wielemaker and Vítor Santos Costa
Portability of Prolog programs: theory and case-studies
Dimitar Shterionov, Angelika Kimmig, Theofrastos Mantadelis and Gerda Janssens
DNF Sampling for ProbLog Inference
Vasco Pedro and Salvador Abreu
Distributed Work Stealing for Constraint Solving
Paulo André and Salvador Abreu
Casting the WAM as an EAM
Gopal Gupta, Neda Saeedloei
Logic Programming Foundations of Cyber-Physical Systems
The Proceedings of CICLOPS-WLPE 2010 have been published electronically at the Computing Research Repository (CoRR).