[TYPES/announce] [fm-announcements] NASA Formal Methods Symposium - NFM 2011 : Third Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] THIRD CALL FOR PAPERS NFM 2011 Third NASA Formal Methods Symposium Pasadena, California, USA April 18 - 20, 2011 http://lars-lab.jpl.nasa.gov/nfm2011 IMPORTANT DATES Submission deadline : *** December 19, 2010 *** Notification of acceptance/rejection : January 21, 2011 Final version due : February 18, 2011 Conference : April 18-20, 2011 THEME The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, government and industry, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. The focus of the symposium is on formal methods, and aims to foster collaboration between NASA researchers and engineers and the wider aerospace and academic formal methods communities. The symposium will be comprised of a mixture of invited talks by leading researchers and practitioners, presentation of accepted papers, and panels. TOPICS OF INTEREST * Theorem proving * Model checking * Real-time, hybrid, stochastic systems * SAT and SMT solvers * Symbolic execution * Abstraction * Compositional verification * Program refinement * Static analysis * Dynamic analysis * Automated testing * Model-based testing * Model-based development * Fault protection * Security and intrusion detection * Application experiences * Modeling and specification formalisms * Requirements specification and analysis INVITED SPEAKERS Rustan Leino Microsoft Research, USA From Retrospective Verification to Forward-Looking Development Oege de Moor University of Oxford, UK Do Coding Standards Improve Software Quality? Andreas Zeller Saarland University, Germany Specifications for Free TUTORIALS Bart Jacobs Katholieke Universiteit Leuven, Belgium VeriFast: a Powerful, Sound, Predictable, Fast Verifier for C and Java Michal Moskal Microsoft Research, USA Verification of Functional Correctness of Concurrent C Programs with VCC HISTORY NFM 2011 is the third edition of the NASA Formal Methods Symposium, organized by NASA on a yearly basis. The first in 2009 and was organized at NASA Ames Research Center, Moffett Field, California. The second in 2010 was organized at NASA head quarters, Washington D.C. The symposium originated from the earlier Langley Formal Methods Workshop series. PAPER SUBMISSION There are two categories of submissions: * Regular paper: up to 15 pages, describing fully developed work and complete results. Papers can present theory, software engineering aspects, or case studies. * Tool papers: up to 6 pages, describing an operational tool. The authors of accepted tool papers will give demonstrations of their tools in tool demo sessions. Tool papers should explain enhancements that have been done compared to previously published work. A tool paper does not need to present the theory behind the tool but can focus more on its features, and how it is used, with screen shots and examples. All papers should be in English and describe original work that has not been published or submitted elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a volume in Lecture Notes of Computer Science. Papers must use the LNCS style, and be in pdf format. COSTS There will be no registration fee charged to participants. PROGRAMME CHAIRS Mihaela Bobaru, NASA/Jet Propulsion Laboratory Klaus Havelund, NASA/Jet Propulsion Laboratory Gerard Holzmann, NASA/Jet Propulsion Laboratory Rajeev Joshi, NASA/Jet Propulsion Laboratory PROGRAMME COMMITTEE Rajeev Alur, University of Pennsylvania, USA Tom Ball, Microsoft Research, USA Howard Barringer, University of Manchester, UK Saddek Bensalem, Verimag Laboratory, France Nikolaj Bjoerner, Microsoft Research, USA Eric Bodden, Technical University Darmstadt, Germany Marsha Chechik, University of Toronto, Canada Rance Cleaveland, University of Maryland, USA Dennis Dams, Bell Labs/Alcatel-Lucent, Belgium Ewen Denney, NASA Ames Research Center, USA Matt Dwyer, University of Nebraska, USA Cormac Flanagan, UC Santa Cruz, USA Dimitra Giannakopoulou, NASA Ames Research Center, USA Patrice Godefroid, Microsoft Research, USA Alex Groce, Oregon State University, USA Radu Grosu, Stony Brook, USA John Hatcliff, Kansas State University, USA Mats Heimdahl, University of Minnesota, USA Mike Hinchey, Lero - the Irish SW. Eng. Research Centre, Ireland Sarfraz Khurshid, University of Texas at Austin, USA Orna Kupferman, Jerusalem Hebrew University, Israel Kim Larsen, Aalborg University, Denmark Rupak Majumdar, Max Planck Institute, Germany Kenneth McMillan, Cadence Berkeley Labs, USA Cesar Munoz, NASA Langley, USA Madan Musuvathi, Microsoft Research, USA Kedar Namjoshi, Bell Labs/Alcatel-Lucent,
[TYPES/announce] [fm-announcements] NFM 2011 - Deadline extension
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PAPERS *** DEADLINE EXTENSION : December 26, 2010 *** NFM 2011 Third NASA Formal Methods Symposium Pasadena, California, USA April 18 - 20, 2011 http://lars-lab.jpl.nasa.gov/nfm2011 IMPORTANT DATES Submission deadline : *** DEADLINE EXTENDED TO: December 26, 2010 *** Notification of acceptance/rejection : January 28, 2011 Final version due : February 18, 2011 Conference : April 18-20, 2011 THEME The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, government and industry, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. The focus of the symposium is on formal methods, and aims to foster collaboration between NASA researchers and engineers and the wider aerospace and academic formal methods communities. The symposium will be comprised of a mixture of invited talks by leading researchers and practitioners, presentation of accepted papers, and panels. TOPICS OF INTEREST * Theorem proving * Model checking * Real-time, hybrid, stochastic systems * SAT and SMT solvers * Symbolic execution * Abstraction * Compositional verification * Program refinement * Static analysis * Dynamic analysis * Automated testing * Model-based testing * Model-based development * Fault protection * Security and intrusion detection * Application experiences * Modeling and specification formalisms * Requirements specification and analysis INVITED SPEAKERS Rustan Leino, Microsoft Research, USA From Retrospective Verification to Forward-Looking Development Oege de Moor, University of Oxford, UK Do Coding Standards Improve Software Quality? Andreas Zeller, Saarland University, Germany Specifications for Free TUTORIALS Andreas Bauer, NICTA and Australian National University, Australia, and Martin Leucker, University of Luebec, Germany The Theory and Practice of SALT - Structured Assertion Language for Temporal Logic Bart Jacobs, Katholieke Universiteit Leuven, Belgium VeriFast: a Powerful, Sound, Predictable, Fast Verifier for C and Java Michal Moskal, Microsoft Research, USA Verification of Functional Correctness of Concurrent C Programs with VCC HISTORY NFM 2011 is the third edition of the NASA Formal Methods Symposium, organized by NASA on a yearly basis. The first in 2009 and was organized at NASA Ames Research Center, Moffett Field, California. The second in 2010 was organized at NASA head quarters, Washington D.C. The symposium originated from the earlier Langley Formal Methods Workshop series. PAPER SUBMISSION There are two categories of submissions: * Regular paper: up to 15 pages, describing fully developed work and complete results. Papers can present theory, software engineering aspects, or case studies. * Tool papers: up to 6 pages, describing an operational tool. The authors of accepted tool papers will give demonstrations of their tools in tool demo sessions. Tool papers should explain enhancements that have been done compared to previously published work. A tool paper does not need to present the theory behind the tool but can focus more on its features, and how it is used, with screen shots and examples. All papers should be in English and describe original work that has not been published or submitted elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a volume in Lecture Notes of Computer Science. Papers must use the LNCS style, and be in pdf format. COSTS There will be no registration fee charged to participants. PROGRAMME CHAIRS Mihaela Bobaru, NASA/Jet Propulsion Laboratory Klaus Havelund, NASA/Jet Propulsion Laboratory Gerard Holzmann, NASA/Jet Propulsion Laboratory Rajeev Joshi, NASA/Jet Propulsion Laboratory PROGRAMME COMMITTEE Rajeev Alur, University of Pennsylvania, USA Tom Ball, Microsoft Research, USA Howard Barringer, University of Manchester, UK Saddek Bensalem, Verimag Laboratory, France Nikolaj Bjoerner, Microsoft Research, USA Eric Bodden, Technical University Darmstadt, Germany Marsha Chechik, University of Toronto, Canada Rance Cleaveland, University of Maryland, USA Dennis Dams, Bell Labs/Alcatel-Lucent, Belgium Ewen Denney, NASA Ames Research Center, USA Matt Dwyer, University of Nebraska, USA Cormac Flanagan, UC Santa Cruz, USA Dimitra Giannakopoulou, NASA Ames Research Center, USA Patrice Godefroid, Microsoft Research, USA Alex Groce, Oregon State University, USA Radu Grosu, Stony Brook, USA John Hatcliff, Kansas State University, USA Mats Heimdahl, University of Minnesota, USA Mike Hinchey, Lero - the Irish SW. Eng. Research Centre, Ireland Sarfraz Khurshid, University
[TYPES/announce] [fm-announcements] CFP - VVPS 2011: Verification and Validation for Planning and Scheduling Systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] -- ** CALL FOR PAPERS ** 3rd ICAPS Workshop on Verification and Validation for Planning and Scheduling Systems (VVPS'11) http://icaps11.informatik.uni-freiburg.de/workshops/vvps.html Freiburg, Germany, June 13, 2011 -- Topic and Objectives *** Planning and scheduling (PS) systems are finding increased application in safety- and mission-critical systems that require a high level of assurance. However, tools and methodologies for verification and validation (VV) of PS systems have received relatively little attention. Therefore, important goals of the workshop are (i) to encourage the ongoing interaction between VV and PS communities, (ii) to identify innovative tools and methodologies (iii) and to elicit open issues and real challenges. The workshop also aims to enhance a stable, long-term establishment of a forum on relevant topics connected to the influence between VV and PS. The workshop series began in 2005 with the first edition of the workshop (http://planning.cis.strath.ac.uk/vvpsws/) during ICAPS '05 and continued in 2009 with the second edition (http://www-vvps09.imag.fr/) during ICAPS '09. These workshops presented a stimulating environment where researchers could discuss about the opportunities and challenges in integrating VV and PS. Topics of interest include: VV of domain models, using technologies such as static analysis, theorem proving, and model checking; consistency and completeness of domain models; domain model coverage metrics; regression, stress and boundary testing; runtime verification of plan executions; generation of robust plans; compositional verification of domain models; how to structure domain models which are more amenable to static analysis; inspection methods; the relationship between timed automata and domain models; investigations of the impact wrt. VV of procedural versus declarative plan models; application of PS techniques to VV; Planning as model checking; etc. Important Dates *** Paper submission: February 11, 2011 Notification of acceptance/rejection: March 11, 2011 Final version due: April 8, 2011 Workshop Date: June 13, 2011 (TBC) Submissions *** There are two types of submissions: short position statements and regular papers. Position papers are a maximum of 2 (two) pages. Regular papers are a maximum of 10 (ten) pages. Papers should be submitted via the VVPS EasyChair website: http://www.easychair.org/conferences/?conf=vvps11 All papers should be typeset in the AAAI style, described at: http://www.aaai.org/Publications/Author/author.php removing AAAI copyright. Accepted papers will be published on the workshop website and printed as a hard-copy. A selection of the accepted papers will be published in a special issue of the International Journal on Software Tools for Technology Transfer: http://sttt.cs.uni-dortmund.de/index.html. Any additional questions can be directed towards the general workshop contact email: vvp...@easychair.org Organization Chairs *** Saddek Bensalem, VERIMAG, France saddek.bensa...@imag.fr Klaus Havelund, NASA JPL, U.S.A. klaus.havel...@jpl.nasa.gov Andrea Orlandini ITIA-CNR, Italy andrea.orland...@itia.cnr.it Programme Committee *** Howard Barringer (University of Manchester, UK) Andreas Bauer (NICTA, Australia) Saddek Bensalem (Verimag/UJF, France) (Co-Chair) Amedeo Cesta (ISTC-CNR, Rome, Italy) Alessandro Cimatti (FBK, Trento, Italy) Alexandre David (Aalborg University, Denmark) Giuseppe Della Penna (University of L'Aquila, L'Aquila, Italy) Lucas Dixon (University of Edinburgh, Edinburgh, UK) Bernd Finkbeiner (Saarland University, Germany) Alberto Finzi (University of Naples, Naples, Italy) Maria Fox (University of Strathclyde, UK) Dimitra Giannakopoulou (NASA Ames Research Center, USA) Enrico Giunchiglia (University of Genova, Italy) Alex Groce (Oregon State University, USA) Klaus Havelund (JPL, USA) (Co-Chair) Gerard Holzmann (JPL, USA) Felix Ingrand (LAAS-CNRS, France) Hadas Kress-Gazit (Cornell University, USA) Kim G. Larsen (Aalborg University, Denmark) Martin Leucker Technische Universität München, Germany) Lee McCluskey (University of Huddersfield, UK) David Musliner (SIFT, USA) Andrea Orlandini (ITIA-CNR, Milan, Italy) (Co-Chair) Corina Pasareanu (NASA Ames Research Center, USA) Charles Pecheur (Université catholique de Louvain, Belgium) Paul Pettersson (Malardalen University, Sweden) Douglas Smith (Kestrel Institute, USA)
