Roberto Bagnara wrote:
>
> Jose Morales wrote:
>> Roberto Bagnara wrote:
>>>
>>> Hi there,
>>>
>>> would you please consider adding to ciao_prolog.h the definition of
>>> macros
>>> allowing to determine the Ciao Prolog version at compile time?
>>> I mean, like the macros
>>>
>>> SICSTUS_MAJOR_VERSION
>>> SICSTUS_MINOR_VERSION
>>> SICSTUS_REVISION_VERSION
>>> SICSTUS_BETA_VERSION
>>>
>>> defined by sicstus.h and the macro
>>>
>>> PLVERSION
>>>
>>> by SWI-Prolog.h.
>> Sorry for the delay in the answer...
>> I have just committed a patch to define
>>
>> CIAO_MAJOR_VERSION
>> CIAO_MINOR_VERSION
>> CIAO_PATCH_VERSION
>> CIAO_SVNREV
>>
>> You can check for older Ciao version by checking
>> that any of them are undefined, e.g.
>>
>> #if !defined(CIAO_MAJOR_VERSION)
>> ...Ciao 1.10...
>> #elif CIAO_MAJOR_VERSION == 1 && CIAO_MINOR_VERSION >= 13
>> ...
>> #endif
>>
>> Please, tell me if it is enough for PPL.
>
> It is, thanks. However, since you probably will not
> stay with SVN forever, I would replace `CIAO_SVNREV'
> by the two macros:
>
> CIAO_VCS (0 for distribution packages, 1 for SVN, 2 for GIT,
> 3 for YOU-NAME-IT, ...)
> CIAO_VCS_REVISION (0 if CIAO_VCS is 0, same as your CIAO_SVNREV
> if CIAO_VCS is 1).
Thanks, that is a good idea! I think that it can be emulated
as follows:
#if defined(CIAO_SVNREV)
#define CIAO_VCS CIAO_VCS__SVN
#define CIAO_VCS_REVISION CIAO_SVNREV
#elif defined(CIAO_GITREV)
...
#endif
so I will not touch it at this moment (unless you need it, of
course).
--Jose
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
Jose Morales wrote:
> Roberto Bagnara wrote:
>>
>>
>> Hi there,
>>
>> would you please consider adding to ciao_prolog.h the definition of
>> macros
>> allowing to determine the Ciao Prolog version at compile time?
>> I mean, like the macros
>>
>> SICSTUS_MAJOR_VERSION
>> SICSTUS_MINOR_VERSION
>> SICSTUS_REVISION_VERSION
>> SICSTUS_BETA_VERSION
>>
>> defined by sicstus.h and the macro
>>
>> PLVERSION
>>
>> by SWI-Prolog.h.
>
> Sorry for the delay in the answer...
> I have just committed a patch to define
>
> CIAO_MAJOR_VERSION
> CIAO_MINOR_VERSION
> CIAO_PATCH_VERSION
> CIAO_SVNREV
>
> You can check for older Ciao version by checking
> that any of them are undefined, e.g.
>
> #if !defined(CIAO_MAJOR_VERSION)
> ...Ciao 1.10...
> #elif CIAO_MAJOR_VERSION == 1 && CIAO_MINOR_VERSION >= 13
> ...
> #endif
>
> Please, tell me if it is enough for PPL.
It is, thanks. However, since you probably will not
stay with SVN forever, I would replace `CIAO_SVNREV'
by the two macros:
CIAO_VCS (0 for distribution packages, 1 for SVN, 2 for GIT,
3 for YOU-NAME-IT, ...)
CIAO_VCS_REVISION (0 if CIAO_VCS is 0, same as your CIAO_SVNREV
if CIAO_VCS is 1).
All the best,
Roberto
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara(a)cs.unipr.it
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
Jose Morales wrote:
> Roberto Bagnara wrote:
>>
>>
>> Hi there,
>>
>> would you please consider adding to ciao_prolog.h the definition of
>> macros
>> allowing to determine the Ciao Prolog version at compile time?
>> I mean, like the macros
>>
>> SICSTUS_MAJOR_VERSION
>> SICSTUS_MINOR_VERSION
>> SICSTUS_REVISION_VERSION
>> SICSTUS_BETA_VERSION
>>
>> defined by sicstus.h and the macro
>>
>> PLVERSION
>>
>> by SWI-Prolog.h.
>
> Sorry for the delay in the answer...
> I have just committed a patch to define
>
> CIAO_MAJOR_VERSION
> CIAO_MINOR_VERSION
> CIAO_PATCH_VERSION
> CIAO_SVNREV
>
> You can check for older Ciao version by checking
> that any of them are undefined, e.g.
>
> #if !defined(CIAO_MAJOR_VERSION)
> ...Ciao 1.10...
> #elif CIAO_MAJOR_VERSION == 1 && CIAO_MINOR_VERSION >= 13
> ...
> #endif
>
> Please, tell me if it is enough for PPL.
It is, thanks. However, since you probably will not
stay with SVN forever, I would replace `CIAO_SVNREV'
by the two macros:
CIAO_VCS (0 for distribution packages, 1 for SVN, 2 for GIT,
3 for YOU-NAME-IT, ...)
CIAO_VCS_REVISION (0 if CIAO_VCS is 0, same as your CIAO_SVNREV
if CIAO_VCS is 1).
All the best,
Roberto
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara(a)cs.unipr.it
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
Roberto Bagnara wrote:
>
>
> Hi there,
>
> would you please consider adding to ciao_prolog.h the definition of macros
> allowing to determine the Ciao Prolog version at compile time?
> I mean, like the macros
>
> SICSTUS_MAJOR_VERSION
> SICSTUS_MINOR_VERSION
> SICSTUS_REVISION_VERSION
> SICSTUS_BETA_VERSION
>
> defined by sicstus.h and the macro
>
> PLVERSION
>
> by SWI-Prolog.h.
Sorry for the delay in the answer...
I have just committed a patch to define
CIAO_MAJOR_VERSION
CIAO_MINOR_VERSION
CIAO_PATCH_VERSION
CIAO_SVNREV
You can check for older Ciao version by checking
that any of them are undefined, e.g.
#if !defined(CIAO_MAJOR_VERSION)
...Ciao 1.10...
#elif CIAO_MAJOR_VERSION == 1 && CIAO_MINOR_VERSION >= 13
...
#endif
Please, tell me if it is enough for PPL.
Cheers,
Jose
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
Hi there,
would you please consider adding to ciao_prolog.h the definition of macros
allowing to determine the Ciao Prolog version at compile time?
I mean, like the macros
SICSTUS_MAJOR_VERSION
SICSTUS_MINOR_VERSION
SICSTUS_REVISION_VERSION
SICSTUS_BETA_VERSION
defined by sicstus.h and the macro
PLVERSION
by SWI-Prolog.h.
Thanks in advance,
Roberto
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara(a)cs.unipr.it
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
We apologize if you receive multiple copies of this email. See below on
how to unsubscribe.
..............................................................
CAV 2008: Call For Participation
=20
Early Registration to CLOSE on
Tuesday, May 27, 2008=20
Hotel Room Block CUTOFF Date
Wednesday, June 4, 2008
=09
20th International Conference on Computer Aided Verification
http://www.princeton.edu/cav2008
July 7 - 14, 2008 Princeton, NJ, USA
=20
..............................................................
CAV 2008 is the 20th in a series dedicated to the advancement of the
theory and practice of computer-aided formal analysis methods for
hardware and software systems.
***** Invited Talks
- James Larus (Microsoft): Singularity: Designing Better Software
- Edmund M. Clarke (CMU), E. Allen Emerson (UT Austin), Joseph Sifakis
(CNRS)
- Edward Felten (Princeton): Coping with Outside-the-Box Attacks=20
***** Invited Tutorials (July 9)
- Harry Foster (Mentor Graphics): Assertion-based Verification
- John Harrison (Intel): Theorem Proving for Verification
- Peter O' Hearn (University of London): Tutorial on Separation Logic
- Reinhard Wilhelm (Saarland University): Abstract Interpretation with
Applications to Timing Validation
=20
***** Affiliated Events
- First CAV Award Presentation
- SMT Competition
- Hardware Model Checking Competition
***** Affiliated Workshops
- Exploiting Concurrency Efficiently and Correctly (EC2)^2: July 7 and 8
http://www.cs.utah.edu/ec2
- Satisfiability Modulo Theories (SMT): July 7 and 8
http://research.microsoft.com/conferences/SMT08/
- Numerical abstractions for Software Verification (NSV): July 8
http://theory.stanford.edu/~srirams/nsv/index.html
- Automated Formal Methods (AFM): July 14
http://fm.csl.sri.com/AFM08/
- Bit-Precise Reasoning (BPR): July 14
http://www.cs.ubc.ca/~babic/index_bpr.htm
- Formal verification of Analog Circuits (FAC): July 14
http://www.em.informatik.uni-frankfurt.de/FAC08.html
- Heap Analysis and Verification (HAV): July 14
http://research.microsoft.com/~jjb/HAV2008/index.html
***** Social Events
- Conference Reception: July 9
- Conference Banquet: July 10
- Manhattan Cruise Excursion: July 12
***** Registration Deadlines
Early registration: May 27
Regular registration: June 21
Late registration: After June 21 and on-site=20
Please follow directions and links on conference website.
***** Accommodations
CAV has arranged special rates at nearby hotels for conference
participants. The cutoff date for Nassau Inn is June 4, and for Hyatt
Regency is June 6.
Dorm rooms on Princeton University campus are also available.=20
Please follow directions and links on conference website.
***** Advance Program (Conference)
----- July 9 (Wednesday) Tutorials Day
8:45 - 9:00 Opening Remarks
9:00 - 10:30 Harry Foster: Assertion-based Verification
10:30 - 11:00 Break I
11:00 - 12:30 John Harrison: Theorem Proving for Verification
12:30 - 2:00 Lunch
2:00 - 3:30 Peter O'Hearn: Tutorial on Separation Logic
3:30 - 4:00 Break II
4:00 - 5:30 Reinhard Wilhelm: Abstract Interpretation with
Applications to Timing Validation
6:00 - 7:30 Conference Reception
=20
----- July 10 (Thursday) =09
8:45 - 9:00 Opening Remarks
9:00 - 10:00 Invited Talk: James Larus -- Singularity: Designing
Better Software
10:00 - 10:30 Break I
10:30 - 12:30 Session 1: Concurrency
10:30 Akash Lal and Thomas Reps: Reducing Concurrent Analysis Under a
Context Bound to Sequential Analysis
11:00 Azadeh Farzan and P. Madhusudan: Monitoring Atomicity in
Concurrent Programs
11:30 Sarvani Vakkalanka, Ganesh Gopalakrishnan and Robert Kirby:
Dynamic Verification of MPI programs with Reductions in Presence of
Split Operations and Relaxed Orderings=20
12:00 Naoki Kobayashi and Davide Sangiorgi: A Hybrid Type System for
Lock-Freedom of Mobile Processes
12:30 - 2:00 Lunch
2:00 - 3:30 Session 2: Memory Consistency
2:00 Surender Baswana, Shashank Mehta and Vishal Powar: Implied Set
Closure and Its Application to Memory Consistency Verification=20
2:30 Sebastian Burckhardt and Madanlal Musuvathi: Effective Program
Verification for Relaxed Memory Models=20
3:00 Ariel Cohen, Amir Pnueli and Lenore Zuck: Mechanical
Verification of Transactional Memories with Non-Transactional Memory
Accesses=20
3:30 - 4:00 Break II
4:00 - 5:30 Special Session
ACM 2007 Turing Award Winners: Edmund Clarke, Allen Emerson, Joseph
Sifakis
6:30 - 10:30 Conference Banquet at Institute for Advanced Study,
Princeton=20
=20
----- July 11 (Friday)
9:00 - 10:30 Session 3: Abstraction/Refinement
9:00 Mihaela Gheorghiu Bobaru, Corina Pasareanu and Dimitra
Giannakopoulou: Automated Assume-Guarantee Reasoning by Abstraction
Refinement=20
9:30 Ariel Cohen and Kedar Namjoshi: Local Proofs for Linear-Time
Properties of Concurrent Programs=20
10:00 Holger Hermanns, Bjorn Wachter and Lijun Zhang: Probabilistic
CEGAR=20
10:30 - 11:00 Break I
11:00 - 12:00 Session 4: Hybrid Systems
11:00 Andre Platzer and Edmund Clarke: Computing Differential Invariants
of Hybrid Systems as Fixedpoints 11:30 Sumit Gulwani and Ashish Tiwari:
Constraint-based Approach for Analysis of Hybrid Systems=20
12:00 - 12:30 Session 5: Tools - Dynamic Verification=20
12:00 Ambar Gadkari, Anand Yeolekar, J Suresh, Ramesh S, Swarup Kumar
Mohalik and K.C. Shashidhar: AutoMOTGen: Automatic Model Oriented Test
Generator for Embedded Control Systems=20
12:15 Andreas Holzer, Christian Schallhart, Michael Tautschnig and
Helmut Veith: FShell: Systematic Test Case Generation for Dynamic
Analysis and Measurement=20
12:30 - 2:00 Lunch
2:00 - 3:30 Session 6: Modeling and Specification Formalisms
2:00 Salil Joshi and Barbara Konig: Applying the Graph Minor Theorem
to the Verification of Graph Transformation Systems=20
2:30 Deepak D'Souza and Madhu Gopinathan: Conflict-Tolerant Features=20
3:00 Rajeev Alur, Aditya Kanade and Gera Weiss: Ranking Automata and
Games for Prioritized Requirements=20
3:30 - 4:00 Break II
4:00 - 5:30 Session 7: Decision Procedures
4:00 Himanshu Jain, Edmund Clarke and Orna Grumberg: Efficient
Interpolation for Linear Diophantine (Dis)equations and Linear Modular
Equations=20
4:30 Ruzica Piskac and Viktor Kuncak: Linear Arithmetic with Stars=20
5:00 Andy King and Harald Sondergaard: Inferring Congruence Equations
with SAT=20
5:30 - 6:30 Session 8: Tools - Decision Procedures
5:30 Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodriguez Carbonell and Albert Rubio: The Barcelogic SMT solver=20
5:45 Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto
Griggio and Roberto Sebastiani: The MathSAT 4 SMT Solver=20
6:00 Dirk Beyer, Damien Zufferey and Rupak Majumdar: CSIsat:
Interpolation for LA+EUF=20
6:15 Laura Meikle and Jacques Fleuriot: Prover's Palette: A
User-Centric Approach to Verification with Isabelle and QEPCAD=20
6:30 - 7:30 CAV Business Meeting
=20
----- July 12 (Saturday)=09
9:00 - 10:00 Invited Talk: Edward Felten -- Coping with
Outside-the-Box Attacks=20
10:00 - 10:30 Break I
10:30 - 12:30 Session 9: Program Verification
10:30 Andreas Podelski, Andrey Rybalchenko and Thomas Wies: Heap
Assumptions On Demand=20
11:00 Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko and
Mooly Sagiv: Proving Conditional Termination=20
11:30 Parosh Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frederic
Haziza and Ahmed Rezine: Monotonic Abstraction for Programs with Dynamic
Memory Heaps=20
12:00 Huu Hai Nguyen and Wei-Ngan Chin: Enhancing Program Verification
with Lemmas=20
12:30 - 1:30 Lunch
1:30 - 3:00 Session 10: Program and Shape Analysis
1:30 Bhargav Gulavani and Sumit Gulwani: A Numerical Abstract Domain
based on "Expression Abstraction" and "Max Operator" with Application in
Timing Analysis=20
2:00 Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno,
Byron Cook, Dino Distefano and Peter O'Hearn: Scalable Shape Analysis
For Systems Code=20
2:30 Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam and
Mooly Sagiv: Thread Quantification for Concurrent Shape Analysis=20
3:00 - 3:30 Break II
3:30 - 4:30 Session 11: Tools - Security and Program
Analysis=20
3:30 Cas Cremers: The Scyther Tool: Verification, Falsification, and
Analysis of Security Protocols=20
3:45 Michael Backes, Stefan Lorenz, Matteo Maffei and Kim Pecina: The
CASPA Tool: Causality-based Abstraction for Security Protocol Analysis=20
4:00 Johannes Kinder and Helmut Veith: Jakstab: A Static Analysis
Platform for Binaries=20
4:15 Stephen Magill, Ming-Hsien Tsai, Peter Lee and Yih-Kuen Tsay:
THOR: A Tool for Reasoning about Shape and Arithmetic=20
4:45 - 11:45 Manhattan Cruise Excursion
=20
------ July 13 (Sunday) Last day of Conference
9:00 - 10:00 Session 12: Hardware Verification I
9:00 Cindy Eisner, Amir Nahir and Karen Yorav: Functional Verification
of Power Gated Designs by Compositional Reasoning=20
9:30 Per Bjesse: A Practical Approach to Word Level Model Checking of
Industrial Netlists
10:00 - 10:30 Break I
10:30 - 11:45 Session 13: Hardware Verification II
10:30 Sudipta Kundu, Sorin Lerner and Rajesh Gupta: Validating High
Level Synthesis=20
11:00 Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz
and Gert-Martin Greuel: An algebraic approach for proving data
correctness in arithmetic data paths=20
11:30 Kavita Ravi, Hyondeuk Kim, Hoonsang Jin, Petr Spacek, Robert P.
Kurshan, Fabio Somenzi and John Pierce: Application of Formal Word-Level
Analysis in Constrained Random Simulation=20
11:45 - 12:00 Hardware Model Checking Competition Report
12:00 - 12:15 SMT-Comp Report
12:15 - 2:00 Lunch
2:00 - 3:00 Session 14: Model Checking
2:00 Sujatha Kashyap and Vijay Garg: Producing short counterexamples
using "crucial events"=20
2:30 Peter Niebert, Doron Peled and Amir Pnueli: Discriminative Model
Checking
3:00 - 4:00 Session 15: Space Efficient Algorithms
3:00 Pavel Simecek, Stefan Edelkamp and Peter Sanders: Semi-External
LTL Model Checking=20
3:30 Rob van Glabbeek and Bas Ploeger: Correcting a Space-Efficient
Simulation Algorithm
4:00 - 4:30 Break II
4:30 - 5:15 Session 16: Tools - Model Checking
4:30 Simon Gay, Rajagopal Nagarajan and Nikolaos Papanikolaou: QMC: A
Model Checker for Quantum Systems=20
4:45 Axel Legay: T(O)RMC: A Tool for (Omega)-Regular Model Checking=20
5:00 Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel and Andreas
Podelski: Faster than Uppaal?=20
5:15 End of Conference
***** Program Committee
- Rajeev Alur, University of Pennsylvania
- Nina Amla, Cadence
- Clark Barrett, New York University
- Armin Biere, JKU Linz
- Roderick Bloem, TU Graz
- Ahmed Bouajjani, University Paris 7
- Alessandro Cimatti, IRST Trento
- Werner Damm, Oldenburg University
- Steven German, IBM
- Ganesh Gopalakrishnan, University of Utah
- Mike Gordon, University of Cambridge
- Orna Grumberg, Technion
- Aarti Gupta (co-chair), NEC Labs America
- David Harel, Weizmann Institute
- John Harrison, Intel
- Thomas A. Henzinger, EPFL
- Holger Hermanns, Saarland University
- Pei-Hsin Ho, Synopsys
- Robert Jones, Intel
- Daniel Kroening, Oxford University
- Orna Kupferman, Hebrew University
- Shuvendu Lahiri, Microsoft Research
- Rupak Majumdar, University of California - Los Angeles
- Oded Maler, Verimag
- Sharad Malik (co-chair), Princeton University
- Ken McMillan, Cadence
- Kedar Namjoshi, Bell Labs, Alcatel-Lucent
- Corina Pasareanu, NASA
- Amir Pnueli, New York University
- Andreas Podelski, University of Freiburg
- Shaz Qadeer, Microsoft Research
- Koushik Sen, University of California - Berkeley
- Fabio Somenzi, University of Colorado
- Ofer Strichman, Technion
- Karen Yorav, IBM Haifa
- Lenore Zuck, University of Illinois
***** Program Chairs
- Aarti Gupta, NEC Labs America
- Sharad Malik, Princeton University
***** Organizing Committee
- Workshops Chair: Byron Cook, Microsoft Research
- Tutorials Chair: Alan Hu, University of British Columbia
***** Local Arrangements
- Webmaster: Nadia Papakonstantinou, NEC Labs America
- Campus Arrangements:
- Tara R. Zarillo, Princeton University
- Stacey Weber Jackson, Princeton University
- Hospitality Crew:
- NEC Labs Verification Group
- Princeton Malik Group
***** Steering Committee
- Edmund M. Clarke, Carnegie Mellon University
- Mike Gordon, University of Cambridge
- Robert P. Kurshan, Cadence
- Amir Pnueli, New York University
***** Sponsors
- Princeton University (http://www.princeton.edu)
- Cadence (http://www.cadence.com)
- IBM (http://www.ibm.com)
- Intel (http://www.intel.com)
- Jasper Design Automation (http://www.jasper-da.com)
- Mentor Graphics (http://www.mentor.com)
- Microsoft Research (http://research.microsoft.com)
- NEC Labs America (http://www.nec-labs.com)
- Synopsys (http://www.synopsys.com)
........................................................................
.=20
We apologize if you receive multiple copies of this email. If you do not
want any further announcements regarding CAV 2008, reply to this email
and put 'UNSUBSCRIBE' in the body or subject of your reply.
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
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.
Logic is a fundamental organizing principle in nearly all areas in Computer
Science. It runs a multifaceted gamut from the foundational to the applied. At
one extreme, it underlies computability and complexity theory and the formal
semantics of programming languages. At the other, it drives billions of gates
every day in the digital circuits of processors of all kinds. Logic is in
itself a powerful programming paradigm but it is also the quintessential
specification language for anything ranging from real-time critical systems to
networked infrastructures. It is logical techniques that link implementation
and specification through formal methods such as automated theorem proving and
model checking. Logic is also the stuff of knowledge representation and
artificial intelligence. Because of its ubiquity, logic has acquired a central
role in Computer Science education.
New results in the fields of computational logic and applications are
welcome. Also welcome are more exploratory presentations, which may examine
open questions and raise fundamental concerns about existing theories and
practices. Topics of interest include, but are not limited to:
* Automated reasoning * Description logics
* Interactive theorem proving * Non-monotonic reasoning
* Implementations of logic * Specification using logics
* Proof assistants * Logic in artificial intelligence
* Program and system verification * Lambda calculus
* Model checking * Constructive logic and type theory
* Rewriting and unification * Computional interpretations of logic
* Logic programming * Logical foundations of programming
* Constraint programming * Logical aspects of concurrency
* Logic and databases * Logic and computational complexity
* Modal and temporal logics * Knowledge representation and reasoning
* Proof-carrying code * Reasoning about actions
* Translation validation * Proof planning
* Logic for the semantic web * Effectively presented structures
* Foundations of security * Logic of distributed systems
Invited Speakers
----------------
It has been a tradition of LPAR to invite some of the most influential
researchers in the focus areas to discuss their work and their vision for
their fields. We are honored that the following members of the community have
accepted this invitation.
* Edmund Clarke, Carnegie Mellon University (USA)
* Amir Pnueli, New York University (USA)
* Michael Backes, Saarland University and MPI-SWS (Germany)
* Thomas Eiter, Technical University of Vienna (Austria)
Submission Instructions
-----------------------
Submissions must not substantially overlap papers that have been published or
that are simultaneously submitted to a journal or a conference with
proceedings. Papers should be submitted in Postscript or Portable Document
Format (PDF); papers submitted in a proprietary word processor format such as
Microsoft Word cannot be considered. Submissions can be of two types:
* Regular papers are meant to describe solid new research results. They
can be up to 15 pages long in LNCS style, including figures, bibliography
and appendices.
* Experimental and tool papers are intended to describe implementations of
systems, to report experiments with implemented systems, or to compare
implemented systems. They can be at most 8 pages long in the LNCS style.
Both types of papers can be electronically submitted by visiting
http://www.easychair.org/conferences/?conf=lpar2008. Prospective authors are
required to register a title and an abstract a week before the paper
submission deadline (see below).
As with the previous editions, the proceedings of LPAR'08 will be published in
Springer-Verlag's Lecture Notes in Computer Science series. They will be
available at the conference.
In keeping with the tradition of LPAR, researchers and practioners are
encouraged to report on interesting work in progress by submitting abstracts
of up to 5 LNCS pages, to be selected for a short-paper session. These
abstracts will not be printed in the proceedings of LPAR'08 and they have a
separate submission deadline (see below).
Participation
-------------
Authors of accepted papers are required to ensure that at least one of them
will be present at the conference. Papers that do not adhere to this policy
will be removed from the proceedings.
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
Program Committee
-----------------
* Franz Baader, TU Dresden (Germany)
* Matthias Baaz, TU Vienna (Austria)
* Peter Baumgartner, National ICT (Australia)
* Josh Berdine, MSR Cambridge (UK)
* Armin Biere, Johannes Kepler University (Austria)
* Iliano Cervesato, Carnegie Mellon University (Qatar) - chair
* Sagar Chaki, Carnegie Mellon SEI (US)
* Hubert Comon-Lundh, ENS Cachan (France)
* Javier Esparza, TU Munich (Germany)
* Orna Grumberg, Technion (Israel)
* Thomas Henzinger, EPFL (Switzerland)
* Joxan Jaffar, NUS (Singapore)
* Juergen Giesl, RWTH Aachen (Germany)
* Claude Kirchner, INRIA & LORIA (France)
* Stephan Kreutzer, Oxford University (UK)
* Orna Kupferman, Hebrew University (Israel)
* Alexander Leitsch, TU Vienna (Austria)
* Nicola Leone, University of Calabria (Italy)
* Cathy Meadows, Naval Research Laboratory (US)
* Heiko Mantel, TU Darmstadt (Germany)
* John Mitchell, Stanford University (US)
* Aart Middeldorp, University of Innsbruck (Austria)
* Andreas Podelski, University of Freiburg (Germany)
* Sanjiva Prasad, IIT Delhi (India)
* Alexander Razborov, Russian Academy of Sciences (Russia)
* Andrey Rybalchenko, MPI-SWS (Germany)
* Ulrike Sattler, University of Manchester (UK)
* Carsten Schuermann, IT University of Copenhagen (Denmark)
* Helmut Seidl, TU Munich (Germany)
* Henny Sipma, Stanford University (US)
* Geoff Sutcliffe, University of Miami (US)
* Ashish Tiwari, SRI (US)
* Helmut Veith, TU Darmstadt (Germany) - chair
* Andrei Voronkov, University of Manchester (UK) - chair
Contact Information
-------------------
Email: lpar08(a)qatar.cmu.edu
Web page: http://www.qatar.cmu.edu/lpar08
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
CALL FOR PAPERS
ICLP'08
24th International Conference on Logic Programming
Udine, Italy, December 9th-13th, 2008
http://iclp08.dimi.uniud.it
CONFERENCE SCOPE
----------------
Since the first conference held in Marseilles in 1982, ICLP has been the
premier international conference for presenting research in logic programming.
Contributions (papers, position papers, and posters) are sought in all areas of
logic programming including but not restricted to:
* Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning,
Knowledge Representation.
* Implementation: Compilation, Memory Management, Virtual Machines, Parallelism.
* Environments: Program Analysis, Program Transformation, Validation and
Verification, Debugging, Profiling, Integration.
* Language Issues: Extensions, Integration with Other Paradigms, Concurrency,
Modularity, Objects, Coordination, Mobility, Higher Order, Types, Modes,
Programming Techniques.
* Related Paradigms: Abductive Logic Programming, Inductive Logic Programming,
Constraint Logic Programming, Answer-Set Programming.
* Applications: Databases, Data Integration and Federation, Software
Engineering, Natural Language Processing, Web and Semantic Web, Agents,
Artificial Intelligence, Bioinformatics
The three broad categories for submissions are:
(1) Technical papers, providing novel research contributions, innovative
perspectives on the field, and/or novel integrations across different
areas;
(2) Application papers, describing innovative uses of logic programming
technology in real-world application domains;
(3) Posters, ideal for presenting and discussing current work, not yet ready
for publication, for PhD thesis summaries and research project overviews.
A separate session dedicated to the celebration of the 20th anniversary of
stable model semantics will also be part of the program.
Accepted papers and posters will be allocated time for presentation during the
conference. At least one author of each accepted submission is expected to
register and participate in the event.
In addition to papers and posters, the technical program will include invited
talks, advanced tutorials, specialized sessions, workshops, and a Doctoral
Student Consortium. Details, as they become available will be posted at:
http://iclp08.dimi.uniud.it
PAPERS AND POSTERS
------------------
Papers and posters must describe original, previously unpublished research, and
must not be simultaneously submitted for publication elsewhere. Emphasis will
be placed on the novelty and innovative nature of the results (even if not
completely polished and refined).
All submissions will be peer-reviewed by an international panel. Submissions
MUST contain substantial original, unpublished material.
All submissions must be written in English. Technical papers and application
papers must not exceed 15 pages in the Springer LNCS format
(see http://www.springeronline.com/lncs/)
The limit for posters is 5 pages in the same format.
The primary means of submission will be electronic, through the Easychair
submission system. The submission page is available at
http://www.easychair.org/conferences/?conf=ICLP08
PUBLICATION
-----------
The proceedings of the conference will be published by Springer-Verlag in the
LNCS series. All accepted papers and posters will be included in the
proceedings.
WORKSHOPS
---------
The ICLP'08 program will include several workshops. They are perhaps the best
place for the presentation of preliminary work, novel ideas, and new open
problems to a more focused and specialized audience. Workshops also provide a
venue for presenting specialised topics and opportunities for intensive
discussions and project collaboration in any areas related to logic
programming, including cross-disciplinary areas.
DOCTORAL CONSORTIUM
-------------------
The Doctoral Consortium (DC) on Logic Programming is the 4th Doctoral
consortium to provide doctoral students with the opportunity to present and
discuss their research directions, and to obtain feedback from both peers and
word-renown experts in the field. The DC will also offer invited speakers and
panel discussions. Accepted participants will receive partial financial support
to attend the event and the main conference. The best paper and presentation
from the DC will be given the opportunity to present in special session of the
main ICLP conference.
CELEBRATING 20th YEARS OF STABLE MODEL SEMANTICS
------------------------------------------------
The year 2008 marks the 20th anniversary of the publication that introduced the
stable model semantics for logic programs with negation. The paper titled "The
stable semantics for logic programs" by Michael Gelfond and Vladimir Lifschitz
was presented at ICLP-1988. It was a momentous event that gave rise to a
vibrant subfield of logic programming known now as the answer-set programming.
Its distinguishing aspects are close connections to the fields of knowledge
representation, satisfiability and constraint satisfaction, ever faster
computational tools, and a growing list of successful applications.
To celebrate the stable-model semantics, there will be a special session at
ICLP 2008 dedicated to answer-set programming. The session will feature talks
by Michael Gelfond and Vladimir Lifschitz. as well as by other major
contributions to the field, presenting personal perspectives on the
stable-model semantics, its impact and its future. There will be a panel
discussion, and regular accepted ICLP papers falling into the answer-set
programming area will complete the program.
CONFERENCE VENUE
----------------
The conference will be held in the city of Udine, the capital of the historical
region of Friuli, Italy. Located between the Adriatic sea and the Alps, close
to Venice, Austria and Slovenia, Udine is a city of Roman origins, funded by
Emperor Otto in 983. Rich of historical sites, Udine is also famous for its
commercial and shopping opportunities and its outstanding wine and culinary
traditions.
SUPPORT SPONSORING AND AWARDS
-----------------------------
The conference is sponsored by the Association for Logic Programming (ALP). The
ALP has funds to assist financially disadvantaged participants. The ALP is
planning to sponsor two awards for ICLP 2008: for the best technical paper and
for the best student paper.
IMPORTANT DATES
--------------- Papers Posters
Abstract submission deadline June 2nd n/a
Submission deadline June 9th August 15th
Notification of authors August 1st September 1st
Camera-ready copy due September 15th September 15th
20 Years of Stable Models TBA
Doctoral Consortium TBA
Workshop Proposals June 2nd
Early-bird Registration TBA
Conference December 9-13, 2008
ICLP'2008 ORGANIZATION
----------------------
General Chair:
Agostino Dovier (University of Udine)
Program Co-Chairs:
Maria Garcia de la Banda (Monash University)
Enrico Pontelli (New Mexico State University)
Workshop Chair:
Tran Cao Son (New Mexico State University)
Doctoral Student Consortium:
David Warren (SUNY Stony Brook)
Tom Schrijvers (K.U.Leuven)
Publicity Co-Chairs:
Marcello Balduccini (Kodak Research Labs)
Alessandro Dal Palu' (University of Parma)
Programming Competition Chair:
Bart Demoen (K.U.Leuven)
20 Years of Stable Models:
Mirek Truszczynski (University of Kentucky)
Andrea Formisano (University of Perugia)
Program Committee:
Salvador Abreu Sergio Antoy
Pedro Barahona Chitta Baral
Gerhard Brewka Manuel Carro
Michael Codish Alessandro Dal Palu'
Bart Demoen Agostino Dovier
John Gallagher Michael Gelfond
Carmen Gervet Gopal Gupta
Manuel Hermenegildo Andy King
Michael Maher Juan Moreno Navarro
Alberto Pettorossi Brigitte Pientka
Gianfranco Rossi Fariba Sadri
Vitor Santos Costa Tran Cao Son
Paolo Torroni Frank Valencia
Mark Wallace
Web Master:
Raffaele Cipriano
Local Arrangements Committee:
Alberto Casagrande
Elisabetta De Maria
Luca Di Gaspero
Carla Piazza
----------------------------------------------------
For further information: iclp08(a)cs.nmsu.eduhttp://iclp08.dimi.uniud.it
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
-------------------------------------------------------------------------------
The CICM Workshop on
Empirically Successful Automated Reasoning for Mathematics (ESARM)
Call for Papers - Submission Deadline - Monday 5th May
------------------------------------------------------
The CICM 2008 Workshop on Empirically Successful Automated Reasoning for
Mathematics (ESARM) will be held as part of the Conferences on Intelligent
Computer Mathematics, in Birmingham, United Kingdom, 26th July - 2nd August,
2008. See the WWW page ...
http://www.cs.miami.edu/~geoff/Conferences/ESARM/
This workshop will bring together practioners and researchers who are
concerned with the development and application of automated reasoning for
mathematics. The workshop will discuss only "really running" systems and
applications, and not theoretical ideas that have not yet been translated
into working software. More details are on the WWW page.
Submission of papers for presentation at the workshop, and proposals for
system and application demonstrations at the workshop, are now invited.
Submissions will be refereed, and a balanced program of high-quality
contributions will be selected. The selected contributions will be printed
as workshop proceedings, and will also be published electronically. The
submission deadline is 5th May, notification of acceptance is on 13th June,
and final versions are due 7th July. Submission details are on the WWW page.
We hope that you will submit a paper, and be part of ESARM.
-------------------------------------------------------------------------------
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------
-------------------------------------------------------------------------------
IJCAR 2008 - The 4th International Joint Conference on Automated Reasoning
Sydney, Australia, 10th - 15th August, 2008
http://2008.IJCAR.org
Calls for Participation, Calls for Workshop Papers, Student Travel Awards
-------------------------------------------------------------------------------
Call for Participation
----------------------
Information about IJCAR's astounding program of invited speakers, technical
papers, workshops, tutorials, competitions, and social events, is available
from the IJCAR WWW pages - 2008.IJCAR.org. There are 101 reasons to attend
IJCAR, which are enumerated on the WWW site. Registration, accomodation, and
travel/visa information is there too. Book your flight to Sydney today!
-------------------------------------------------------------------------------
Calls for Workshop Papers, Tutorial Participation
-------------------------------------------------
There will be six workshops and four tutorials before IJCAR, 10th and 11th
August. See their individual WWW pages, linked from the IJCAR WWW pages, for
submission and participation information.
+ Workshops
- The 5th International Verification Workshop (VERIFY'08)
- Practical Aspects of Automated Reasoning (PAAR-2008)
- Evaluation of Systems for Higher Order Logic (ESHOL)
- Complexity, Expressibility, & Decidability in Automated Reasoning (CEDAR'08)
- Constraints in Formal Verification
- Combining Systems for Efficient and Scalable Reasoning (CoSyScaRe 08)
+ Tutorials
- Introduction to Nominal Isabelle - Christian Urban
- Formal Methods in Use at Galois, Inc. - Joe Hurd
- SMT Solvers in Program Analysis and Verification - Nikolaj Bjorner and
Leonardo de Moura
- Coalgebraic Logics and Applications (COALA) - Dirk Pattinson
-------------------------------------------------------------------------------
Student Travel Awards
---------------------
Two award schemes that provide sponsorhips to support student attendance at
IJCAR are available. See the IJCAR WWW pages for details.
-------------------------------------------------------------------------------
==============================================================================
Message: Address: Action:
help majordomo(a)clip.dia.fi.upm.es Info. on useful commands
subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list
unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list
<whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list
-----------------------------------------------------------------------------
Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/
-----------------------------------------------------------------------------