Ciao-users May 2008

ciao-users@cliplab.org

5 participants
10 discussions

Re: Ciao version in ciao_prolog.hh
by Jose Morales 29 May '08

29 May '08

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/ -----------------------------------------------------------------------------

1 0

Re: Ciao version in ciao_prolog.hh
by Roberto Bagnara 29 May '08

29 May '08

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/ -----------------------------------------------------------------------------

1 0

Re: Ciao version in ciao_prolog.hh
by Roberto Bagnara 29 May '08

29 May '08

1 0

Re: Ciao version in ciao_prolog.hh
by Jose Morales 29 May '08

29 May '08

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/ -----------------------------------------------------------------------------

1 0

Ciao version in ciao_prolog.hh
by Roberto Bagnara 26 May '08

26 May '08

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/ -----------------------------------------------------------------------------

1 0

CAV 08 CFP: Early Registration to CLOSE on May 27
by Aarti Gupta 23 May '08

23 May '08

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/ -----------------------------------------------------------------------------

1 0

LPAR Call for Papers
by geoff＠cs.miami.edu 21 May '08

21 May '08

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/ -----------------------------------------------------------------------------

1 0

ICLP'08 CALL FOR PAPERS
by ICLP 08 09 May '08

09 May '08

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.edu http://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/ -----------------------------------------------------------------------------

1 0

Automated Reasoning in Mathematics
by geoff＠cs.miami.edu 08 May '08

08 May '08

------------------------------------------------------------------------------- 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/ -----------------------------------------------------------------------------

1 0

IJCAR Calls and Awards
by geoff＠cs.miami.edu 08 May '08

08 May '08

------------------------------------------------------------------------------- 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/ -----------------------------------------------------------------------------

1 0

2026

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

Ciao-users May 2008