December 2011 - Haskell

ANNOUNCE: ioctl 0.0.1
by Maciej Piechotka 13 Sep '15

13 Sep '15

A package for type-safe I/O control. Currently only ioctl is supported. Currently simply a extract from my tuntap fork TODO: - Return the integer as well as structure (will break the API) - Port for Windows Network.Socket.IOCtl (as soon as I manage to setup some sane environment on this platform) - Wrapping around DeviceIoControl Example (in hsc): data NotRead = NotRead instance NotRead Int where ioctlReq _ = #const FIONREAD notRead s = ioctlsocket' s NotRead Regards

2 1

CFP: Term and Graph rewriting, special issue of MSCS
by Rachid Echahed 13 Feb '14

13 Feb '14

-------------------------------------------------------------------------- First Call for Papers Special Issue of Mathematical Structures in Computer Science (MSCS) on "TERM and GRAPH Rewriting" -------------------------------------------------------------------------- Scope -------------------------------------------------------------------------- Rewriting techniques constitute a foundational theory of computing science. They are being investigated for several structures such as lambda-terms, first-order terms or graphs and have been successfully used in many areas such as programming languages, automated reasoning, program verification, security, etc. This is witnessed by the leading international events ICGT, RTA or TLCA among others. During the last decade, a particular interest has been devoted to the study of the impact of shared structures in term and graph rewriting through the international editions of TERMGRAPH series of workshops. Sharing is indeed ubiquitous in several research areas, for instance: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the modelling of biological or chemical abstract machines, the implementation techniques of programming languages. Term and graph rewriting are also used in automated theorem proving and symbolic computation systems working on shared structures... This special issue is devoted to recent developments in all aspects of TERM and GRAPH rewriting. This includes (but is not limited to): term rewriting, graph transformation, proof methods, programming languages, infinitary rewriting, rewrite strategies, semantics, properties of rewriting ... -------------------------------------------------------------------------- Submissions -------------------------------------------------------------------------- Submitted papers must be original and not submitted for publication elsewhere, and will be subject to the standard journal refereeing process of the Mathematical Structures in Computer Science (MSCS) journal. Submissions should be in pdf format following the MSCS instruction for contributors (http://assets.cambridge.org/MSC/MSC_ifc.pdf) and should be submitted electronically via the following easy-chair web site: https://www.easychair.org/conferences/?conf=mscsrewriting2012 -------------------------------------------------------------------------- Important Dates -------------------------------------------------------------------------- January 20, 2012 : Abstract submission February 20, 2012: Paper submission June 15, 2012 : Notification of acceptance -------------------------------------------------------------------------- Guest Editor: -------------------------------------------------------------------------- Rachid Echahed, CNRS LIG Lab., Grenoble, France echahed(a)imag.fr --------------------------------------------------------------------------

1 8

ANNOUNCE: GHC version 7.2.1
by Ian Lynagh 26 Mar '12

26 Mar '12

============================================================= The (Interactive) Glasgow Haskell Compiler -- version 7.2.1 ============================================================= The GHC Team is pleased to announce a new major release of GHC, 7.2.1. The 7.2 branch is intended to be more of a "technology preview" than normal GHC stable branches; in particular, it supports a significantly improved version of DPH, as well as new features such as compiler plugins and "safe Haskell". The design of these new features may evolve as we get more experience with them. See the release notes for more details of what's new and what's changed. We are also using this branch as an opportunity to work out the best workflows to use with git. We expect the 7.2 branch to be short-lived, with 7.4.1 coming out shortly after ICFP as normal. Full release notes are here: http://www.haskell.org/ghc/docs/7.2.1/html/users_guide/release-7-2-1.html How to get it ~~~~~~~~~~~~~ The easy way is to go to the web page, which should be self-explanatory: http://www.haskell.org/ghc/ We supply binary builds in the native package format for many platforms, and the source distribution is available from the same place. Packages will appear as they are built - if the package for your system isn't available yet, please try again later. Background ~~~~~~~~~~ Haskell is a standard lazy functional programming language. GHC is a state-of-the-art programming suite for Haskell. Included is an optimising compiler generating good code for a variety of platforms, together with an interactive system for convenient, quick development. The distribution includes space and time profiling facilities, a large collection of libraries, and support for various language extensions, including concurrency, exceptions, and foreign language interfaces (C, whatever). GHC is distributed under a BSD-style open source license. A wide variety of Haskell related resources (tutorials, libraries, specifications, documentation, compilers, interpreters, references, contact information, links to research groups) are available from the Haskell home page (see below). On-line GHC-related resources ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Relevant URLs on the World-Wide Web: GHC home page http://www.haskell.org/ghc/ GHC developers' home page http://hackage.haskell.org/trac/ghc/ Haskell home page http://www.haskell.org/ Supported Platforms ~~~~~~~~~~~~~~~~~~~ The list of platforms we support, and the people responsible for them, is here: http://hackage.haskell.org/trac/ghc/wiki/Contributors Ports to other platforms are possible with varying degrees of difficulty. The Building Guide describes how to go about porting to a new platform: http://hackage.haskell.org/trac/ghc/wiki/Building Developers ~~~~~~~~~~ We welcome new contributors. Instructions on accessing our source code repository, and getting started with hacking on GHC, are available from the GHC's developer's site run by Trac: http://hackage.haskell.org/trac/ghc/ Mailing lists ~~~~~~~~~~~~~ We run mailing lists for GHC users and bug reports; to subscribe, use the web interfaces at http://www.haskell.org/mailman/listinfo/glasgow-haskell-users http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs There are several other haskell and ghc-related mailing lists on www.haskell.org; for the full list, see http://www.haskell.org/mailman/listinfo/ Some GHC developers hang out on #haskell on IRC, too: http://www.haskell.org/haskellwiki/IRC_channel Please report bugs using our bug tracking system. Instructions on reporting bugs can be found here: http://www.haskell.org/ghc/reportabug

4 3

Open PhD and PostDoc positions at Marburg University
by Klaus Ostermann 04 Jan '12

04 Jan '12

ear all, we are happy to announce that we have new openings at the PhD and PostDoc level. The Programming Language and Software Technology Group, headed by Klaus Ostermann, conducts research dedicated to developing new technologies that help to construct high-quality software in a productive way. We use and develop an exciting set of technologies involving functional, object-oriented, domain-specific and aspect-oriented programming languages, software product lines, parser technology, language-integrated queries, static and dynamic software analysis, type systems, and many other topics. For more information consult http://www.uni-marburg.de/fb12/ps/ We offer positions with a lot of freedom to choose and develop research topics, few obligations, collaboration with a very strong group of researchers, competitive salary, and opportunities to develop a strong academic career path (e.g. by founding their own junior research group). For the PostDoc positions, we expect applicants to have demonstrated scientific excellence in areas related to our own research. For PhD positions, we expect evidence of the potential for scientific excellence. Knowledge of German is not required; the communication language in our group is English. Marburg is an attractive small "student town" right in the center of Germany. We are only an hour ride away from Frankfurt Airport, which will bring you to many destinations worldwide in a single hop. To apply for a position, please send informal inquiries to Klaus Ostermann (contact data can be found on our website). We are flexible with regard to the starting date, but generally the sooner the better. We are looking forward to hearing from you. Best wishes, Klaus Ostermann on behalf of the PS group at Marburg University http://www.uni-marburg.de/fb12/ps

2 1

ANN: LocallyLazyRead-0.1
by e.ex.exi.exit＠googlemail.com 21 Dec '11

21 Dec '11

ANN: LocallyLazyRead-0.1 Repository: http://www.patch-tag.com/r/exit/LocallyLazyRead/home (no hackage package since anonymous uploads are not allowed there) The package comprises just one function which applies a lazy parser to a resource that may otherwise be accessed via strict IO: > import Control.LocallyLazyRead Assume a (lazy) parser: > parse :: Read a => String -> IO (a,String) > parse = return . head . reads Turn this into a "get"-like function which reads the characters strictly but computes the parse result lazily: > foo :: Handle -> IO (String,Char,(Int,Int),Char) > foo h = do > s <- llread (hGetChar h) parse > c1 <- hGetChar h > ii <- llread (hGetChar h) parse > c2 <- hGetChar h > return (s,c1,ii,c2) where llread is of type IO t -> ([t] -> IO (a,[t])) -> IO a The parser must satisfy the following semantic constraint: For all finite p, arbitrary q, arbitrary a with the right type: (parse (p++q)) computes the value (a,q) in a given IO state if and only if (parse p) computes the value (a,[]) in the same IO state This entails zero lookahead into the unparsed rest, and also a rest which truely depends on the input - parse x = return (x,[]) is forbidden. Violations are detected at runtime: > -- throws a LookaheadAttempt exception: > bar :: Handle -> IO Bool > bar h = llread (hGetChar h) (\(y:ys)-> return (isSpace y,y:ys)) > -- throws a Lookahead exception: > barbar :: Handle -> IO Int > barbar h = llread (hGetChar h) parse --- e(x(i(t))) <e.ex.exi.exit(a)gmail.com> Key fingerprint = A915 1EA1 4D0E 759A B925 0076 A409 2713 E490 3776

1 0

ANNOUNCE: partial-lens 0.0.1
by roconnor＠theorem.ca 21 Dec '11

21 Dec '11

Do you miss null references from your old imperative programming days? Wish that the worlds best imperative language had null references? Now your wishes have come true with the new partial-lens package! partial-lens augment edwardk's data-lens package with partial lens. Partial lenses are like regular lenses but have the possibility of not referencing anything. In other words, null references are possible. One notable different with null references from this package is that you can set them without getting a run-time error. Instead setting a null reference is a no-op; however it is possible to determine if setting failed from the return value of the assignment operation. Actually I don't have any applications for partial lenses myself, so if you find this library useful, please let me know. I wrote this mostly because we know what partial lenses are in theory (they are the coalgebras of the (Identity :+: Store b) comonad) but I wanted to see what a real library would look like. -- Russell O'Connor <http://r6.ca/> ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

1 0

PADL 2012 Final Call for Participation
by Claudio Russo 20 Dec '11

20 Dec '11

Final Call for Participation ============================ 14th International Symposium on Practical Aspects of Declarative Languages (PADL 2012) http://research.microsoft.com/~crusso/padl12 Philadelphia, Pennsylvania, USA, January 23-24, 2012 Co-located with ACM POPL'12 You are cordially invited to PADL'12. PADL is a forum for researchers and practitioners to present original work emphasizing novel applications and implementation techniques for all forms of declarative concepts, including functional, logic and constraints. PADL'12 is sponsored by Association for Logic Programming with cooperation of ACM SIGPLAN and support by Microsoft Research. Registration ============ To register for PADL'12, please follow the instructions at: https://regmaster3.com/2012conf/POPL12/register.php The early registration deadline is December 24, 2011. The registration fee will cover a copy of the symposium proceedings, refreshments, and an informal dinner. Hotel Information ================= PADL will be co-located with POPL at the Sheraton Society Hill Hotel in Philadelphia. Please visit POPL's web site to make reservations at the special conference rate. Program ======= The symposium will include invited talks by Boon Thau Loo and Don Stewart, and 19 technical papers selected from 41 submissions. The preliminary program is as follows: Invited Talk (9:00-10:00) * Boon Thau Loo Recent Advances in Declarative Networking Break (10:00-10:30) Session 1: Applications (10:30-12:00) * Mayer Goldberg and Guy Wiener A Declarative Approach for Software Modeling * Sergio Antoy and Michael Hanus Contracts and Specifications for Functional Logic Programming * Pedro M. Martins, Julie A. McCann and Susan Eisenbach The Environment as an Argument Lunch (not provided) (12:00-13:30) Session 2: Logic Programming (13:30-15:30) * Yuliya Lierler, Shaden Smith, Mirek Truszczynski and Alex Westlund Weighted-Sequence Problem: ASP vs CASP and Declarative vs Problem-Oriented Solving * Marcello Balduccini and Yuliya Lierler Practical and Methodological Aspects of the Use of Cutting-Edge ASP Tools * Christian Theil Have and Henning Christiansen Efficient tabling of structured data using indexing and program transformation * Dario Campagna, Beata Sarna-Starosta and Tom Schrijvers Optimizing Inequality Joins in Datalog with Approximated Constraint Propagation Break (15:30-16:00) Session 3: Parallelism and Concurrency (16:00-17:30) * Elvira Albert, Puri Arenas and Miguel Gomez-Zamalloa Symbolic Execution of Concurrent Objects in CLP * Pablo Chico De GuzmÃ¡n, Amadeo Casas, Manuel Carro and Manuel Hermenegildo A Segment-Swapping Approach for Executing Trapped Computations * Michael Lesniak Palovca: Describing and Executing Graph Algorithms in Haskell Informal PADL Dinner (Place: TBA) Tuesday, January 24, 2012 Breakfast (8:00-9:00) Invited Talk (9:00-10:00) * Don Stewart Make Things Now! Pragmatic Functional Programming in Haskell Break (10:00-10:30) Session 4: Domain Specific Languages I (10:30-12:00) * Kenny Zhu, Kathleen Fisher and David Walker LearnPADS++: Incremental Inference of Ad Hoc Data Formats * Jeroen Bransen, Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra The Kennedy-Warren algorithm revisited: ordering Attribute Grammars * Nicholas Coleman Distributed Policy Specification and Interpretation with Classified Advertisements Lunch (not provided) (12:00-13:30) Session 5: Domain Specific Languages II (13:30-15:30) * Andy Gill and Bowe Neuenschwander Handshaking in Kansas Lava using Patch Logic * Daniel Winograd-Cort, Hai Liu and Paul Hudak Virtualizing Real-World Objects in FRP * Edwin Brady and Kevin Hammond Resource-safe Systems Programming with Embedded Domain Specific Languages * David Broman and Henrik Nilsson Node-Based Connection Semantics for Equation-Based Object-Oriented Modeling Languages Break (15:30-16:00) Session 6: Numerics (16:00-17:00) * Paul Tarau A Declarative Specification of Tree-based Symbolic Arithmetic Computations * Vincent St-Amour, Sam Tobin-Hochstadt, Matthew Flatt and Matthias Felleisen Typing the Numeric Tower

1 0

CfP: Extended Submission Deadline TAP 2012 (International Conference on Test and Proofs)
by Achim D. Brucker 20 Dec '11

20 Dec '11

(Apologies for duplicates) ************************************************************ *** TAP 2012 offers extended submission deadlines due to *** *** numerous requests received: *** *** Abstract submission: January 11, 2012 *** *** Paper submission: January 18, 2012 *** ************************************************************ *** TAP 2012 solicits both full papers and (industrial) *** *** experience/tool papers *** *** in combining proofs and (security) testing. *** ************************************************************ CALL FOR PAPERS Full and short Research Paper, Industrial Experience Papers, Tool Papers Abstract submission: Jan 11, 2012, Paper submission Jan 18, 2012 6th INTERNATIONAL CONFERENCE ON TEST AND PROOFS (TAP 2012) http://lifc.univ-fcomte.fr/tap2012/ May 31 - June 1, 2012, Prague, Czech Republic Part of the TOOLS Federated Conferences 2012 http://tools2012.fit.cvut.cz/ The TAP conference is devoted to the convergence of proofs and tests, to the application of techniques from both sides and their combination for the advancement of software quality. Test and Proof seem to be contradictory techniques: if you have proved your program to be correct, it is fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope to prove its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities. However, the development of both approaches lead to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity. Further evidence give test data generation techniques from models or programs which boil down to constraint resolution techniques for relatively large formula; the advent of powerful SMT solvers have therefore powered new testing techniques. Finally, since formal, proof-based verification is costly, testing invariants and background theories can be helpful to detect errors early and to improve cost effectivity. Summing up, in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. The TAP conference aims to bring together researchers and practitioners working in the converging fields of testing and proving, and will offer a generous allocation of papers, panels and informal discussions. Topics of interest cover theory definitions, tool constructions and experimentations and include (other topics related to TAP are welcome): - Transfer of concepts from testing to proving (e.g., coverage criteria) and from proving to testing - Program proving with the aid of testing techniques - New problematics in automated reasoning emerging from specificities of test generation - Verification and testing techniques combining proofs and tests - Generation of test data, oracles, or preambles by deductive techniques such as: theorem proving, model checking, symbolic execution, constraint logic programming - Model-based testing and verification - Generation of specifications by deduction - Automatic bug finding - Debugging of programs combining static and dynamic analysis - Formal frameworks - Tool descriptions and experience reports - Case studies combining tests and proofs - Applying combination of test and proof techniques to new application domains such as validating security procotols or vulnerability detection of programs Important Dates: ================ Abstract submission (extended): January 11, 2012 Paper submission (extended): January 18, 2012 Notification: March 2, 2012 Camera ready version: March 19, 2012 TAP conference: May 31 - June 1, 2012 TOOLS conferences (TOOLS, ICMT, SC, TAP): May 29 - June 01, 2012 Conference Chairs: Bertrand Meyer Program Chairs: Achim D. Brucker and Jacques Julliand Program Committee (to be extended): =================================== Nazareno Aguirre, Bernhard K. Aichernig, Paul Ammann, Dirk Beyer, Nikolaj Bjorner, Robert Clarisó, Marco Comini, Catherine Dubois, Gordon Fraser, Angelo Gargantini, Alain Giorgetti, Patrice Godefroid, Martin Gogolla, Arnaud Gotlieb, Reiner Hähnle, Bart Jacobs, Thierry Jéron, Gregory Kapfhammer, Nikolai Kosmatov, Victor Kuliamin, Karl Meinke, Jeff Offutt, Holger Schlingloff, T.H. Tse, Margus Veanes, Luca Viganò, Burkhart Wolff, Fatiha Zaidi Submission: =========== Please submit your papers via http://lifc.univ-fcomte.fr/tap2012/. TAP 2012 will accept two types of papers: - Research papers: full papers with at most 16 pages in LNCS format (pdf), which have to be original, unpublished and not submitted elsewhere. - Short contributions: work in progress, (industrial) experience reports or tool demonstrations, position statements; an extended abstract with at most 6 pages in LNCS format (pdf) is expected. Accepted papers will be published in the Springer LNCS series and will be available at the conference. The contents of previous TAP proceedings is available at: http://www.informatik.uni-trier.de/~ley/db/conf/tap/ -- Dr. Achim D. Brucker, SAP Research, Vincenz-Priessnitz-Str. 1, D-76131 Karlsruhe Phone: +49 6227 7-52595, Fax: +49-6227 78-50502, http://www.brucker.ch

1 0

CFP: Automation of Software Test 2012
by John Hughes 19 Dec '11

19 Dec '11

(It would be nice to see some papers on Haskell automated testing here) John AST 2012 7th IEEE/ACM International Workshop on Automation of Software Test http://ast2012.org At ICSE 2012 (http://www.ifi.uzh.ch/icse2012/) Zurich, Switzerland, 2-3 June 2012 IMPORTANT DATES: Submission deadline: February 17, 2012 Notification of acceptance: March 19, 2012 Camera-Ready version: March 29, 2012 Workshop dates: June 2 - 3 2012 In software development practice, testing accounts for as much as 50% of the total development effort. It is therefore imperative to reduce the cost and improve the effectiveness of software testing by automating the testing process. In the past decades, a great amount of research effort has been spent on automatic test case generation, automatic test oracles, etc. Test automation is also becoming an important part of software testing practice. The workshop is the 7th edition of the successful AST workshops held at ICSE 2006-2011. It will provide researchers and practitioners with a forum for exchanging ideas, experiences, understanding of the problems, visions for the future, and promising solutions to the problems. The workshop will also provide a platform for researchers and developers of testing tools to work together to identify the problems in the theory and practice of software test automation and to set an agenda and lay the foundation for future development. TOPICS OF INTEREST The workshop focuses on bridging the gap between the theory and practice of software test automation. The topics of interest include, but are not limited to, the following: 1) Methodology: Software test automation in the context of various software development methodologies, such as model-driven, component-based, agile, test-driven, product lines, service-oriented, agent-oriented, and aspect-oriented methodologies, and in evolutionary development. 2) Technology: Automation of test techniques and methods used in test-related activities, support for software testing methods, and applications to specific types of software in different application domains. 3) Software testing tools and environments: Issues in the development, operation, maintenance and evolution of software testing tools and environments. 4) Experiments, empirical studies and experience reports and vision of the future of software test automation. The AST 2012 workshop focuses on a special topic on the Automation of Security Testing. Submissions on this topic are especially encouraged, but papers on other topics are also welcome. CHARETTE DISCUSSIONS The workshop continues the successful charette discussions of previous years. This year, the charette discussion sessions will focus on the topic of automation of security testing. INDUSTRIAL CASE STUDIES There will also be an Industrial Case Studies session at the workshop, with presentations reporting the real state of the practice in automation of software testing. Test practitioners are especially encouraged to contribute their experiences and insights on test automation. Topics for this session include, but are not limited to, the following: new tools, new best practices, process innovations related to test automation, gaps in existing vendor toolsets, ideas and visions for near-term research work. SUBMISSIONS Two types of submissions are invited: regular papers and industrial case study papers. The former presents research in the area of software test automation, while the latter presents practical applications of test automation. Both types of papers are limited to 7 pages in IEEE Conference Proceedings Format. All papers submitted to the workshop must be unpublished original work and should not be simultaneously under review or submitted elsewhere. All submissions must be in English and in either PDF or postscript format through online upload to the workshop submission website at the following URL: http://www.easychair.org/conferences/?conf=AST2012 All submissions will be reviewed by three PC members. Regular papers will be judged on the basis of their clarity, relevance, originality, and contribution. Case study papers will be judged on the basis of their clarity, relevance, and interest to the workshop participants. PUBLICATION OF PAPERS The accepted workshop papers including both regular and case study papers will be published in the AST 2012 Proceedings and included in the IEEE Digital Libraries. Workshop attendees will receive a memory stick with both ICSE 2012 and AST 2012 proceedings on it. The presentations slides will be published on the AST 2012 website. Authors of accepted papers are required to register for the workshop and present the paper at the workshop in order for the paper to be included in the proceedings and Digital Libraries. A journal special issue to publish revised and extended versions of selected best papers is pending.

1 0

CAV 2012: Call For Papers
by CAV 2012 CFP 19 Dec '11

19 Dec '11

====== CALL FOR PAPERS ====== 24th International Conference on Computer Aided Verification (CAV 2012) July 7-13, 2012 Berkeley, California, USA Program Chairs: Madhusudan Parathasarathy and Sanjit A. Seshia Website: http://cav12.cs.illinois.edu/ Aims and Scope ------------------- The conference on Computer Aided Verification (CAV), 2012, is the 24th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as biological systems and computer security. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers will be invited to a special issue of Formal Methods in System Design and the Journal of the ACM. Topics of interest include: - Algorithms and tools for verifying models and implementations - Hardware verification techniques - Hybrid systems and embedded systems verification - Deductive, compositional, and abstraction techniques for verification - Program analysis and software verification - Testing and runtime analysis based on verification technology - Verification methods for parallel and concurrent hardware/software systems - Applications and case studies in verification - Verification in industrial practice - Algorithms and tools for system synthesis - Verification techniques for security - Formal models and methods for biological systems ** NEW in 2012 ** CAV will have *special tracks* in the following four areas: 1. Hardware Verification (track chair: Andreas Kuehlmann) 2. Computer Security (track chair: Somesh Jha) 3. Embedded Systems (track chair: Stavros Tripakis) 4. SAT and SMT (track chair: Daniel Kroening) Submissions in these four topics are especially encouraged. Papers in these areas will be subject to the same rigorous review process as other papers. Accepted special track papers will be organized into special sessions that are highlighted in the program. Events --------- The conference will include the following events: * Pre-conference workshops on July 7-8. * The main conference will take place July 9th-13th: -- Invited tutorials on July 9th. -- Technical sessions on July 10-13. Please see the conference website for further details. Paper Submission -------------------- There are two categories of submissions: A. Regular Papers: Submissions, not exceeding sixteen (16) pages using Springer's LNCS format, should contain original research, and sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data available with their submission. Submissions reporting on case studies in an industrial context are strongly invited, and should describe details, weaknesses, and strengths in sufficient depth. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. B. Tool Presentations: Submissions, not exceeding six (6) pages using Springer's LNCS format, should describe the implemented tool and its novel features. An appendix that will not be part of the published presentation may be added for use in the program committee selection process. A demonstration, in a separate demonstration session, is expected to accompany a tool presentation. Papers describing tools that have already been presented (in any conference) will be accepted only if significant and clear enhancements to the tool are reported and implemented. Papers exceeding the stated maximum length run the risk of rejection without review. Note that the page limit for submissions has been increased to 16 pages. For regular papers, an appendix can be joined to the submissions providing additional material such as details on proofs or experiments. The appendix is not guaranteed to be read or taken into account by the reviewers and it should not contain information necessary to the understanding and the evaluation of the presented work. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. Papers must be submitted in PDF format. Submission is done with EasyChair. Information about the submission procedure will be available at: http://cav12.cs.illinois.edu/ Important Dates - Abstract submission: January 15, 2012 - Paper submission (firm): January 22, 2012 at 23:59 Samoa time (UTC/GMT-11) - Author feedback/rebuttal period: March 7-9, 2012 - Notification of acceptance/rejection: March 22, 2012 - Final version due: April 20, 2012 Program Chairs ------------------ Madhusudan Parthasarathy, University of Illinois at Urbana-Champaign, USA Sanjit A. Seshia, University of California at Berkeley, USA Program Committee --------------------- Rajeev Alur (Univ. Pennsylvania) Roderick Bloem (TU Graz) Supratik Chakraborty (IIT Bombay) Swarat Chaudhuri (Rice Univ.) Adam Chlipala (MIT) Vincent Danos (University of Edinburgh) Thomas Dillig (College of William and Mary) Andy Gordon (Microsoft Research) Mike Gordon (Cambridge Univ.) Orna Grumberg (Technion) Aarti Gupta (NEC Labs) William Hung (Synopsys) Somesh Jha (Univ. Wisconsin) Ranjit Jhala (UCSD) Bengt Jonsson (Uppsala Univ.) Rajeev Joshi (NASA JPL) Daniel Kroening (Oxford Univ.) Andreas Kuehlmann (Coverity) Viktor Kuncak (EPFL) Shuvendu Lahiri (Microsoft Research) Rupak Majumdar (MPI-SWS) Ken Mcmillan (Microsoft Research) David Molnar (Microsoft Research) Kedar Namjoshi (Bell Labs) Albert Oliveras (TU Catalonia, Barcelona) Joel Ouaknine (Oxford Univ.) Gennaro Parlato (Univ. of Southampton) Madhusudan Parthasarathy (UIUC) Nir Piterman (Univ. of Leicester) Andreas Podelski (Univ. of Freiburg) Shaz Qadeer (Microsoft Research) Zvonimir Rakamaric (Univ. of Utah) Sriram Sankaranarayanan (Univ. of Colorado) Sanjit A. Seshia (UC Berkeley) Natasha Sharygina (Univ. of Lugano) Stavros Tripakis (UC Berkeley) Helmut Veith (TU Vienna) Mahesh Viswanathan (UIUC) Jin Yang (Intel) Karen Yorav (IBM) Steering Committee ---------------------- Michael Gordon, University of Cambridge, UK Orna Grumberg, Technion, Israel Robert Kurshan, Cadence Design Systems, USA Kenneth McMillan, Microsoft Research, USA CAV Award ------------ The annual CAV Award has been established for a specific fundamental contribution or a series of outstanding contributions to the field of Computer Aided Verification. The award of $10,000 will be granted to an individual or a group of individuals chosen by the Award Committee from a list of nominations. The Award Committee may choose to make no award. The CAV Award shall be presented in an award ceremony at CAV and a citation will be published in a Journal of Record (currently, Formal Methods in System Design). Call for Nominations for the CAV Award ------------------------------------------ Anyone can submit a nomination. The Award Committee can originate a nomination. Anyone, with the exception of members of the Award Committee, is eligible to receive the Award. A nomination must state clearly the contribution(s), explain why the contribution is fundamental or the series of contributions is outstanding, and be accompanied by supporting letters and other evidence of worthiness. Nominations should include a proposed citation (up to 25 words), a succinct (100-250 words) description of the contribution(s), and a detailed statement to justify the nomination. The cited contribution(s) must have been made not more recently than five years ago and not over twenty years ago. In addition, the contribution(s) should not yet have received recognition via a major award, such as the ACM Turing or Kanellakis Awards. The nominee may have received such an award for other contributions. The 2012 CAV Award Committee consists of Thomas A. Henzinger (Chair) Rajeev Alur Marta Kwiatkowska Aarti Gupta The nominations should be sent to Thomas Henzinger at tah(a)ist.ac.at. Nominations must be received by January 22, 2012.

1 0