http://blog.gmane.org/gmane.comp.mathematics.hol hourly 1 1901-01-01T00:00+00:00 http://gmane.org/img/gmane-25t.png http://gmane.org http://comments.gmane.org/gmane.comp.mathematics.hol/2706 <pre>===================================================== ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13) http://complogic.cs.mcgill.ca/lfmtp13 23 September, 2013 Boston, USA Co-located with with ICFP'13 CALL FOR PAPERS ===================================================== IMPORTANT DATES Paper submission: June 14, 2013 Author notification: July 7, 2013 Final versions due: July 18, 2013 ===================================================== Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical framework. The broad subject areas of LFMTP'13 are: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical frameworks, contextual frameworks, functional programming over logical frameworks. This year's invited speaker are Dale Miller (Inria) and Robert Harper (CMU) . In addition, this year LFMTP will celebrate the twenty years anniversary of the publication of: Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993 Program Committee: ================= * David Baelde, ENS * James Cheney, Edinburgh * Adam Chlipala, MIT * Dan Licata, CMU/IAS * Alberto Momigliano, Milano (organizer) * Brigitte Pientka, McGill (organizer) * Nicolas Pouillard ITU * Randy Pollack, Harvard (organizer) * Andrei Popescu, TUM * Florian Rabe, Bremen * Stephanie Weirich, UPenn Submission Details: ============ In addition to regular papers, we also solicit "work in progress" report, in a broad sense. Those do not need to report original or fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style guidelines (9pt format, more details appear on the symposium web page). The length is restricted to 12 pages, except for "Work in Progress" papers, which are restricted to 6 pages. Submission is via EasyChair: https://www.easychair.org/conferences/?conf=lfmtp2013 Proceedings: ============ Accepted (regular) papers will be included in the ACM Digital Library. Authors are encouraged to publish auxiliary material with their paper (technical appendixes, source code, scripts, test data, etc.). Travel Support: =============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC program, see its web page (http://www.sigplan.org/PAC.htm). ------------------------------------------------------------------------------ Try New Relic Now &amp; We'll Send You this Cool Shirt New Relic is the only SaaS-based application performance monitoring service that delivers powerful full stack analytics. Optimize and monitor your browser, app, &amp; servers with just a few lines of code. Try New Relic and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Brigitte Pientka 2013-05-22T03:06:39 http://comments.gmane.org/gmane.comp.mathematics.hol/2705 <pre>25th OpenMath Workshop Bath, UK 10 July 2013 co-located with CICM 2013 Submission deadline 7 June http://www.cicm-conference.org/2013/openmath/ OBJECTIVES OpenMath (http://www.openmath.org) is a language for exchanging mathematical formulae across applications (such as computer algebra systems). From 2010 its importance has increased in that OpenMath Content Dictionaries were adopted as a foundation of the MathML 3 W3C recommendation (http://www.w3.org/TR/MathML), the standard for mathematical formulae on the Web. Topics we expect to see at the workshop include * Feature Requests (Standard Enhancement Proposals) and Discussions for going beyond OpenMath 2; * Further convergence of OpenMath and MathML 3; * Reasoning with OpenMath; * Software using or processing OpenMath; * OpenMath on the Semantic Web; * New OpenMath Content Dictionaries; Contributions can be either full research papers, Standard Enhancement Proposals, or a description of new Content Dictionaries, particularly ones that are suggested for formal adoption by the OpenMath Society. IMPORTANT DATES (all times are "anywhere on earth") * 7 June: Submission * 20 June: Notification of acceptance or rejection * 5 July: Final revised papers due * 10 July: Workshop SUBMISSIONS Submission is via EasyChair (http://www.easychair.org/conferences?conf=om20131). Final papers must conform to the EasyChair LaTeX style. Initial submissions in this format are welcome but not mandatory – but they should be in PDF and within the given limit of pages/words. Submission categories: * Full paper: 5–10 EasyChair pages * Short paper: 1–4 EasyChair pages * CD description: 1-6 EasyChair pages; a .zip or .tgz file of the CDs must be attached, or a link to the CD provided. * Standard Enhancement Proposal: 1-10 EasyChair pages (as appropriate w.r.t. the background knowledge required); a .zip or .tgz file of any related implementation (e.g. a Relax NG schema) should be attached. If not in EasyChair format, 500 words count as one page. PROCEEDINGS Electronic proceedings will be published with CEUR-WS.org. ORGANISATION COMMITTEE * Christoph Lange (University of Birmingham, UK) * James Davenport (University of Bath, UK) * Michael Kohlhase (Jacobs University Bremen, Germany) PROGRAMME COMMITTEE * Lars Hellström (Umeå Universitet, Sweden) * Jan Willem Knopper (Technische Universiteit Eindhoven, Netherlands) * Paul Libbrecht (Center for Educational Research in Mathematics and Technology, Martin-Luther-University Halle-Wittenberg) (to be completed) Comments/questions/enquiries: to be sent to openmath-workshop&lt; at &gt;googlegroups.com </pre> Christoph LANGE 2013-05-20T11:10:28 http://comments.gmane.org/gmane.comp.mathematics.hol/2704 <pre>*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line* ********************************************************************* 2013 INTERNATIONAL SUMMER SCHOOL ON TRENDS IN COMPUTING SSTiC 2013 Tarragona, Spain July 22-26, 2013 Organized by Rovira i Virgili University http://grammars.grlmc.com/SSTiC2013/ ********************************************************************* +++ next registration deadline: May 26 +++ ********************************************************************* AIM: SSTiC 2013 will be an open forum for the convergence of top class well recognized computer scientists and people at the beginning of their research career (typically PhD students) as well as consolidated researchers. SSTiC 2013 will cover the whole spectrum of computer science by means of 63 six-hour courses dealing with hot topics at the frontiers of the field. By actively participating, lecturers and attendees will share the idea of scientific excellence as the main motto of their research work. ADDRESSED TO: Graduate students from around the world. There are no pre-requisites in terms of the academic degree the attendee must hold. However, since there will be several levels among the courses, in the description of some of them reference may be made to specific knowledge background. SSTiC 2013 is appropriate also for people more advanced in their career who want to keep themselves updated on developments in the field. Finally, senior researchers will find it fruitful to listen and discuss with people who are main references of the diverse branches of computing nowadays. REGIME: 7 parallel sessions will be held during the whole event. Participants will be able to freely choose the courses they will be willing to attend as well as to move from one to another. VENUE: Palau Firal i de Congressos de Tarragona Arquitecte Rovira, 2 43001 Tarragona http://www.palaucongrestgna.com COURSES AND PROFESSORS: Divyakant Agrawal (Santa Barbara) [intermediate] Scalable Data Management in Enterprise and Cloud Computing Infrastructures Shun-ichi Amari (Riken) [introductory] Information Geometry and Its Applications James Anderson (Chapel Hill) [intermediate] Scheduling and Synchronization in Real-Time Multicore Systems Pierre Baldi (Irvine) [intermediate] Big Data Informatics Challenges and Opportunities in the Life Sciences Yoshua Bengio (Montréal) [introductory/intermediate] Deep Learning of Representations Stephen Brewster (Glasgow) [advanced] Multimodal Human-Computer Interaction Bruno Buchberger (Linz) [introductory] Groebner Bases: An Algorithmic Method for Multivariate Polynomial Systems. Foundations and Applications Rajkumar Buyya (Melbourne) [intermediate] Cloud Computing Jan Camenisch (IBM Zurich) [intermediate] Cryptography for Privacy Jeffrey S. Chase (Duke) [intermediate] Trust Logic as an Enabler for Secure Federated Systems Larry S. Davis (College Park) [intermediate] Video Analysis of Human Activities Paul De Bra (Eindhoven) [intermediate] Adaptive Systems Marco Dorigo (Brussels) [introductory] An Introduction to Swarm Intelligence and Swarm Robotics Paul Dourish (Irvine) [introductory] Ubiquitous Computing in a Social Context Max J. Egenhofer (Maine) [introductory/intermediate] Qualitative Spatial Relations: Formalizations and Inferences Richard M. Fujimoto (Georgia Tech) [introductory] Parallel and Distributed Simulation David Garlan (Carnegie Mellon) [advanced] Software Architecture: Past, Present and Future Mario Gerla (Los Angeles) [intermediate] Vehicle Cloud Computing Georgios B. Giannakis (Minnesota) [advanced] Sparsity and Low Rank for Robust Data Analytics and Networking Ralph Grishman (New York) [intermediate] Information Extraction from Natural Language Francisco Herrera (Granada) [intermediate] Imbalanced Classification: Current Approaches and Open Problems Paul Hudak (Yale) [introductory] Euterpea: From Signals to Symphonies Using Haskell Niraj K. Jha (Princeton) [intermediate] FinFET Circuit Design George Karypis (Minnesota) [introductory] Introduction to Parallel Computing: Architectures, Algorithms, and Programming Aggelos K. Katsaggelos (Northwestern) [intermediate/advanced] Sparsity-based Advances in Image Processing Arie E. Kaufman (Stony Brook) [advanced] Advances in Visualization Carl Kesselman (Southern California) [intermediate] Biomedical Informatics and Big Data Hugo Krawczyk (IBM Research) [intermediate] An Introduction to the Design and Analysis of Authenticated Key Exchange Protocols Pierre L'Ecuyer (Montréal) [intermediate] Quasi-Monte Carlo Methods in Simulation: Theory and Practice Laks Lakshmanan (British Columbia) [intermediate/advanced] Information and Influence Spread in Social Networks Wenke Lee (Georgia Tech) [introductory] DNS-based Monitoring of Malware Activities Maurizio Lenzerini (Roma La Sapienza) [intermediate] Ontology-based Data Integration Ming C. Lin (Chapel Hill) [introductory/intermediate] Physically-based Modeling and Simulation Jane W.S. Liu (Academia Sinica) [intermediate] Critical Information and Communication Technologies for Disaster Preparedness and Response Satoru Miyano (Tokyo) [intermediate] How to Hack Cancer Systems with Computational Methods Aloysius K. Mok (Austin) [intermediate] From Real-time Systems to Cyber-physical Systems Hermann Ney (Aachen) [intermediate/advanced] Probabilistic Modelling for Natural Language Processing - with Applications to Speech Recognition, Handwriting Recognition and Machine Translation Cathleen A. Norris (North Texas) &amp; Elliot Soloway (Ann Arbor) [introductory] Primary &amp; Secondary Educational Computing in the Age of Mobilism Jeff Offutt (George Mason) [intermediate] Cutting Edge Research in Engineering of Web Applications David Padua (Urbana) [intermediate] Parallel Programming with Abstractions Bijan Parsia (Manchester) [introductory] The Semantic Web: Conceptual and Technical Foundations Massoud Pedram (Southern California) [intermediate] Energy Efficient Architectures and Information Processing Systems Charles E. Perkins (FutureWei) [intermediate/advanced] Beyond 4G Prabhakar Raghavan (Google) [introductory/intermediate] Web Search and Advertising Sudhakar M. Reddy (Iowa) [introductory] Design for Test and Test of Digital VLSI Circuits Phillip Rogaway (Davis) [introductory/intermediate] Provably Secure Symmetric Encryption Gustavo Rossi (La Plata) [intermediate] Topics in Model Driven Web Engineering Kaushik Roy (Purdue) [introductory/intermediate] Low-energy Computing Robert Sargent (Syracuse) [introductory] Validating Models Douglas C. Schmidt (Vanderbilt) [intermediate] Patterns and Frameworks for Concurrent and Networked Software Bart Selman (Cornell) [intermediate] Fast Large-scale Probabilistic and Logical Inference Methods Mubarak Shah (Central Florida) [intermediate/advanced] Visual Crowd Surveillance Ron Shamir (Tel Aviv) [introductory] Revealing Structure in Disease Regulation and Networks Satinder Singh (Ann Arbor) [introductory/advanced] Reinforcement Learning: On Machines Learning to Act from Experience Dawn Xiaodong Song (Berkeley) [introductory] Selected Topics in Computer Security Mike Thelwall (Wolverhampton) [introductory] Sentiment Strength Detection for the Social Web Julita Vassileva (Saskatchewan) [introductory/intermediate] Engaging Users in Social Computing Systems Philip Wadler (Edinburgh) [introductory] Topics in Lambda Calculus and Life Yao Wang (Polytechnic New York) [introductory/advanced] Video Compression: Fundamentals and Recent Development Gio Wiederhold (Stanford) [introductory] Software Economics: How Do the Results of the Intellectual Efforts Enter the Global Market Place Limsoon Wong (National Singapore) [introductory/intermediate] The Use of Context in Gene Expression and Proteomic Profile Analysis Michael Wooldridge (Oxford) [introductory] Autonomous Agents and Multi-Agent Systems Ronald R. Yager (Iona) [introductory/intermediate] Fuzzy Sets and Soft Computing Philip S. Yu (Illinois Chicago) [advanced] Mining Big Data REGISTRATION: It has to be done at http://grammars.grlmc.com/SSTiC2013/Registration.php Since the capacity of the venue is limited, registration requests will be processed on a first come first served basis. The registration period will be closed when the capacity of the venue will be complete. FEES: They are the same (a flat rate) for all people by the corresponding deadline. They give the right to attend all courses. ACCOMMODATION: Information about accommodation is available on the website of the School. CERTIFICATE: Participants will be delivered a certificate of attendance. IMPORTANT DATES: Announcement of the programme: January 26, 2013 Six registration deadlines: February 26, March 26, April 26, May 26, June 26, July 26, 2013 QUESTIONS AND FURTHER INFORMATION: Lilica Voicu: florentinalilica.voicu&lt; at &gt;urv.cat POSTAL ADDRESS: SSTiC 2013 Research Group on Mathematical Linguistics (GRLMC) Rovira i Virgili University Av. Catalunya, 35 43002 Tarragona, Spain Phone: +34-977-559543 Fax: +34-977-558386 ACKNOWLEDGEMENTS: Ajuntament de Tarragona Diputació de Tarragona Universitat Rovira i Virgili ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d </pre> GRLMC 2013-05-19T20:04:00 http://comments.gmane.org/gmane.comp.mathematics.hol/2703 <pre>::: ECSCW 2013 ::: Doctoral Colloquium The 13th European Conference on Computer Supported Cooperative Work (ECSCW 2013) 21-25 September 2013, Paphos, Cyprus http://www.ecscw2013.org/ The ECSCW 2013 Doctoral Colloquium provides an opportunity for doctoral students to discuss their research in an international forum, under the guidance of a panel of experienced CSCW researchers. The Doctoral Colloquium will be held on Sunday the 22nd of September 2013 as part of the 13th European Conference on Computer Supported Cooperative Work in Paphos, Cyprus (http://www.ecscw2013.org). We invite students who are working in the broad field of CSCW to apply. The strongest candidates will be those students who have a well-established research proposal, have made some progress towards it, but are still on time to benefit from advice and feedback by peers and senior colleagues. Selected candidates will be expected to give short, informal presentations of their work during the Colloquium, to be followed by extensive group discussion in a friendly and constructive workshop. To apply please submit the following documents 1) A 4-page overview of your doctoral research, stating your research questions, level of advancement, and expected contributions. Formatting instructions and paper templates are available at http://ecscw2013.cs.ucy.ac.cy/templates.zip. The submissions are not anonymous and should therefore include names, affiliations and contact information. 2) A short (2-3 paragraph) biography. 3) A paragraph that articulates what you expect to gain from attending the ECSCW 2013 Doctoral Colloquium. 4) An email letter from your supervisor indicating that they support your application to the ECSCW 2013 Doctoral Colloquium and that they agree that your research is at an appropriate stage for participation. These letters should also indicate how you and other students might benefit from your participation in the colloquium. The e-mail should be sent to ecscw13dc&lt; at &gt;umbc.edu stating "ECSCW Doctoral Colloquium: + YOUR NAME" in the subject heading. All items should be submitted as PDF files through easychair https://www.easychair.org/conferences/?conf=ecscw2013 Item 1 should be submitted separately, items 2 and 3 should be submitted as a single PDF file. IMPORTANT DATES ·Submission Deadline: 15 June 2013 (5:00pm PDT) using EasyChair ·Notification Date: 22 June 2013 ·Camera-Ready Deadline: 26 September 2013 DC CHAIRS Antonella De Angeli, University of Trento, Trento, Italy Wayne Lutters, University of Maryland, Baltimore County, USA Contact: ecscw13dc&lt; at &gt;umbc.edu -------------------------------------------------------------------- This is not SPAM. If you want to be removed from this list, please send an email to [announce&lt; at &gt;cs.ucy.ac.cy] with the single word 'remove' in the subject of the email. ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Announce Announcements 2013-05-19T10:23:52 http://comments.gmane.org/gmane.comp.mathematics.hol/2701 <pre>------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Jose A Martin 2013-05-17T11:03:32 http://comments.gmane.org/gmane.comp.mathematics.hol/2698 <pre>--------------------------------------------------------------------------- COMPUTABILITY IN EUROPE 2013: The Nature of Computation Milan, Italy, July 1 - 5, 2013 CALL FOR PARTICIPATION Informal Presentation Deadline: 31 May 2013 Early Registration Deadline: 31 May 2013 http://cie2013.disco.unimib.it co-located with Unconventional Computation and Natural Computation 2013 http://ucnc2013.disco.unimib.it --------------------------------------------------------------------------- TUTORIAL SPEAKERS: Gilles Brassard (Universite de Montreal) and Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and University of Colorado at Boulder) PLENARY TALKS: Ulle Endriss (University of Amsterdam) Lance Fortnow (Georgia Institute of Technology) Anna Karlin (University of Washington) Bernard Moret (Ecole Polytechnique Federale de Lausanne) Mariya Soskova (Sofia University) Endre Szemeredi (Hungarian Academy of Sciences, Rutgers University) SPECIAL SESSIONS: * Algorithmic Randomness (organizers: Mathieu Hoyrup, Andre Nies) Speakers: Johanna Franklin (University of Connecticut, USA), Noam Greenberg (Victoria University, New Zealand), Joseph S. Miller (University of Wisconsin, USA), Nikolay Vereshchagin (Moscow State University, Russia) * Computational Complexity in the Continuous World (organizers: Akitoshi Kawamura, Robert Rettinger) Speakers: Mark Braverman (Princeton University, USA), Daniel S. Graca (Universidade do Algarve), Joris van der Hoeven (Ecole polytechnique, France), Chee K. Yap (New York University, USA) * Computational Molecular Biology (organizers: Alessandra Carbone, Jens Stoye) Speakers: Sebastian Boecker (University of Jena, Germany), Marilia D. V. Braga (Inmetro, Brazil), Andrea Pagnani (Human Genetics Foundation, Italy), Laxmi Parida (IBM Thomas J. Watson Research Center, USA) * Computation in Nature (organizers: Mark Daley, Natasha Jonoska) Speakers: Jerome Durand-Lose (Univ. of Orleans, France), Giuditta Franco (Univ. of Verona Italy), Lila Kari (Univ. of Western Ontario, Canada), Darko Stefanovic (Univ. of New Mexico, USA) * Data Streams and Compression (organizers: Paolo Ferragina, Andrew McGregor) Speakers: Graham Cormode (AT&amp;T Labs, USA), Irene Finocchi (University of Rome, Italy), Andrew McGregor (University of Massachusetts, USA), Marinella Sciortino (University of Palermo, Italy). * History of Computation (organizers: Gerard Alberts, Liesbeth De Mol) Speakers: David Alan Grier (George Washington University, USA), Thomas Haigh (University of Wisconsin, USA), Ulf Hashagen (Deutsches Museum, Germany), Matti Tedre (Stockholm University, Sweden). CiE serves as an interdisciplinary forum for research in all aspects of computability and foundations of computer science, as well as the interplay of these theoretical areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics. Women in Computability Workshop, July 2, 2013: We continue the programme "Women in Computability" supported by the journal "Annals of Pure and Applied Logic" (Elsevier). Speakers: Irene Finocchi, Laxmi Parida, Liesbeth De Mol The Women in Computability workshop aims to bring together women in Computing and Mathematical research to present and exchange their academic and scientific experience with young researchers. The meeting will offer the CIE scientific community the opportunity to encourage young students, especially young female researchers, to have active careers in the mathematical and computational sciences. INFORMAL PRESENTATIONS: Continuing the tradition of past CiE conferences, this year's CiE conference endeavours to get the best of both worlds. In addition to the formal presentations based on our LNCS proceedings volume, we invite researchers to present informal presentations. For this, please send us a brief description of your talk (between one paragraph and one page) by the DEADLINE: MAY 31, 2013 Please submit your abstract electronically, via EasyChair &lt;https://www.easychair.org/login.cgi?conf=cie2013&gt;, selecting the category "Informal Presentation". You will be notified whether your talk has been accepted for informal presentation usually within a week after your submission. **** Also authors of abstracts accepted for presentation are invited to submit a paper extending the abstract to the journal Computability **** __________________________________________________________________________ ASSOCIATION COMPUTABILITY IN EUROPE http://www.computability.org.uk CiE Conference Series http://www.illc.uva.nl/CiE CiE 2013 http://cie2013.disco.unimib.it CiE Membership Application Form http://www.cs.swan.ac.uk/acie __________________________________________________________________________ ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d </pre> S B Cooper 2013-05-16T12:06:38 http://comments.gmane.org/gmane.comp.mathematics.hol/2697 <pre>I am practicing using HOL4. As a beginner, a lot of primary problems puzzle me. There is the code of n-bit adder I writed according the paper of "Hardware verification using higher-order logic". I have proved the basis case, and stopped at the step case. set_trace "Unicode" 0; show_assums:=true; open HolKernel boolLib Parse bossLib; open listTheory; load "listlib"; open listlib; open arithmeticTheory; (***********************************************************************) (* *) (* n-bit adder *) (* *) (* Data structure: *) (* First input: bool list *) (* Second input: bool list *) (* Carry input: bool *) (* Sum output: bool list *) (* Carry output: bool *) (* *) (***********************************************************************) (***********************************************************************) (* Get the n-th element of the bool list *) (***********************************************************************) val NTH_BIT_def = Define `(NTH_BIT(n:num,[]) = F) /\ (NTH_BIT(0,l:bool list) = HD l) /\ (NTH_BIT(n:num,l:bool list) = NTH_BIT(n-1,TL l))`; (***********************************************************************) (* Computing value of the n-th element of the list *) (* ture then 1,or 0 *) (***********************************************************************) val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:bool list) = if(NTH_BIT(n,l)) then 1 else 0`; (***********************************************************************) (* Computing value of the bool element *) (* ture then 1,or 0 *) (***********************************************************************) val BIT_VAL_def = Define `BIT_VAL(aBIT:bool) = if(aBIT) then 1 else 0`; (***********************************************************************) (* Computing value of the whole list *) (***********************************************************************) val VALUE_def = Define `(VALUE(0,l:bool list) = NTH_BIT_VAL(0,l)) /\ (VALUE(SUC n:num,l:bool list)= (2 ** (SUC n)) * NTH_BIT_VAL(n,l) + VALUE(n,l))`; (***********************************************************************) (* Sum output of the n-th bit *) (***********************************************************************) val OUT_def = Define`OUT(n,inp1,inp2,cn,out) = (NTH_BIT(n,out) = (~NTH_BIT(n,inp1) /\ ~NTH_BIT(n,inp2) /\ cn) \/ (~NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2) /\ ~cn) \/ (NTH_BIT(n,inp1) /\ ~(NTH_BIT(n,inp2)) /\ ~cn) \/ (NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2) /\ cn))`; (***********************************************************************) (* Carry of the n-th bit *) (***********************************************************************) val COUT_def = Define`COUT(n,inp1,inp2,cn,cout) = (cout = (NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2)) \/ (NTH_BIT(n,inp1) /\ cn) \/ (NTH_BIT(n,inp2) /\ cn))`; (***********************************************************************) (* The implementation of (n+1)-th full adder *) (***********************************************************************) val FULL_ADDER_IMP_def = Define`FULL_ADDER_IMP(SUC n,inp1,inp2,cn,out,cout) = (OUT(n,inp1,inp2,cn,out) /\ COUT(n,inp1,inp2,cn,cout))`; (***********************************************************************) (* Implementation of n-bit adder *) (***********************************************************************) val NADDER_IMP_def = Define`(NADDER_IMP(0,inp1,inp2,cin,out,cout) = (cout = cin)) /\ (NADDER_IMP(SUC n,inp1,inp2,cin,out,cout) = (?cn:bool. NADDER_IMP(n,inp1,inp2,cin,out,cn) /\ FULL_ADDER_IMP(SUC n,inp1,inp2,cn,out,cout)))`; (***********************************************************************) (* Specification of n-bit adder *) (***********************************************************************) val NADDER_SPEC_def = Define`NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout) = ((2**(SUC n))*BIT_VAL(cout) + VALUE(n,out) = VALUE(n,inp1)+VALUE(n,inp2)+BIT_VAL(cin))`; (***********************************************************************) (* Main goal *) (***********************************************************************) g`!n:num inp1:bool list inp2:bool list cin:bool out:bool list cout:bool.((LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ (LENGTH inp1 &gt; n) /\ NADDER_IMP(SUC n,inp1,inp2,cin,out,cout)) ==&gt; NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout)`; (***********************************************************************) (* Basis case *) (***********************************************************************) e(Induct); e(REPEAT GEN_TAC THEN REWRITE_TAC [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,BIT_VAL_def,OUT_def,COUT_def,VALUE_def]); e(SIMP_TAC bool_ss []); e(Cases_on `cin`); e(Cases_on `inp1`); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(RW_TAC list_ss []); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(Cases_on `h`); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `inp1`); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(RW_TAC list_ss []); e(Cases_on `inp2`); e(RW_TAC list_ss []); e(Cases_on `h`); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(Cases_on `h'`); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); (***********************************************************************) (* Step case *) (***********************************************************************) e(REPEAT GEN_TAC); e(REWRITE_TAC [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,OUT_def,COUT_def,BIT_VAL_def,VALUE_def]); We will simple the goal as follows. Question 1:How to eliminate the existential quantifier "cn"? Question 2:How to use the following assumption in the hypothesis list? !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) I do not know how to apply the tactic to the assumption. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; SUC n /\ (?cn. (?cn'. NADDER_IMP (n,inp1,inp2,cin,out,cn') /\ (NTH_BIT (n,out) &lt;=&gt; ~NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ cn' \/ ~NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ ~cn' \/ NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ ~cn' \/ NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ cn') /\ (cn &lt;=&gt; NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) \/ NTH_BIT (n,inp1) /\ cn' \/ NTH_BIT (n,inp2) /\ cn')) /\ (NTH_BIT (SUC n,out) &lt;=&gt; ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ cn \/ ~NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ ~cn \/ NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ ~cn \/ NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ cn) /\ (cout &lt;=&gt; NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) \/ NTH_BIT (SUC n,inp1) /\ cn \/ NTH_BIT (SUC n,inp2) /\ cn)) ==&gt; (2 ** SUC (SUC n) * (if cout then 1 else 0) + (2 ** SUC n * NTH_BIT_VAL (n,out) + VALUE (n,out)) = 2 ** SUC n * NTH_BIT_VAL (n,inp1) + VALUE (n,inp1) + (2 ** SUC n * NTH_BIT_VAL (n,inp2) + VALUE (n,inp2)) + if cin then 1 else 0) ------------------------------------ !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) : proof So, I try to apply RW_TAC to the goal,then get 64 subgoals. e(RW_TAC list_ss [BIT_VAL_def,OUT_def,COUT_def,VALUE_def,NTH_BIT_def,NTH_BIT_VAL_def,NADDER_SPEC_def,NADDER_IMP_def,FULL_ADDER_IMP_def]); The subgoal at the top goal stack as follows. VALUE (n,out) + (2 ** SUC n + 2 ** SUC (SUC n)) = VALUE (n,inp1) + (VALUE (n,inp2) + (2 * 2 ** SUC n + 1)) ------------------------------------ 0. !inp1 inp2 cin out cout. (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ LENGTH inp1 &gt; n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==&gt; NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) 1. NTH_BIT (n,out) 2. NTH_BIT (n,inp1) 3. NTH_BIT (n,inp2) 4. LENGTH inp1 = LENGTH inp2 5. LENGTH inp2 = LENGTH out 6. LENGTH inp1 &gt; SUC n 7. NADDER_IMP (n,inp1,inp2,T,out,T) 8. NTH_BIT (SUC n,out) &lt;=&gt; ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) \/ NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) 9. NTH_BIT (SUC n,inp1) 10. NTH_BIT (SUC n,inp2) : proof I can not move forward. thx! ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Yuntao Peng 2013-05-16T13:11:31 http://comments.gmane.org/gmane.comp.mathematics.hol/2696 <pre>The talks at NFM 2013 will be webcast live starting May 14th, 8:00 AM Pacific Standard Time. All the NFM 2013 talks can be viewed at http://www.ustream.tv/channel/nasa-arc The program for NFM 2013 is available at http://ti.arc.nasa.gov/events/nfm-2013/program/ Neha --- To opt-out from this mailing list, send an email to fm-announcements-request&lt; at &gt;lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner&lt; at &gt;lists.nasa.gov ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d </pre> Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGTInc.)] 2013-05-14T13:28:17 http://comments.gmane.org/gmane.comp.mathematics.hol/2694 <pre>A number list stored a set of numbers, the number value may be 0 or 1, no other case, now, I want to get the value of n-th element of the list. If n is greater than the length of the list,then fail. I don't know how to throw the exception which defined by myself. The function defined as follows: val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l l)) else (failwith "n is greater than list's LENGTH")`; Exception raised at TotalDefn.Define: between line 40, character 31 and frag 0 row 0 col 137: at TotalDefn.defnDefine: The following variables are free in the right hand side of the proposed definition: "failwith" ! Uncaught exception: ! HOL_ERR val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l l)) else fail()`; Exception raised at TotalDefn.Define: on line 41, characters 30-159: at TotalDefn.defnDefine: The following variables are free in the right hand side of the proposed definition: "fail" ! Uncaught exception: ! HOL_ERR however, I define function using ML, done. - fun nth_bit_val n l = if(n=0) then fail() else l; thx ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Yuntao Peng 2013-05-14T03:46:14 http://comments.gmane.org/gmane.comp.mathematics.hol/2693 <pre>********************************************************************* *** Federated Conference on Rewriting, Deduction, and Programming *** *** RDP 2013 *** *** June 23 - June 28, 2013 *** *** Eindhoven, The Netherlands *** *** http://www.win.tue.nl/rdp2013/ *** *** *** *** CALL FOR PARTICIPATION *** *** *** ********************************************************************* ************* EARLY REGISTRATION CLOSES ON JUNE 1 ************* --------------------------------------------------------------------- </pre> Luca Paolini 2013-05-14T07:53:45 http://comments.gmane.org/gmane.comp.mathematics.hol/2691 <pre>[ NOTE: We have delayed our submission dates by a week to bring ourselves into line with our co-conference, APLAS. Come to sunny Australia to escape the northern winter! ] CALL FOR PAPERS =============== Third International Conference on Certified Programs and Proofs (CPP 2013) -------------------------------------------------------------------------- December 2013, Australia (co-located with APLAS 2013) CPP is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. The first two CPP conferences were held in Kenting, Taiwan, and Kyoto, Japan, in December 2011 and 2012, respectively. As with the first meetings, the proceedings will be published in Springer-Verlag’s Lecture Notes in Computer Science series. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; teaching mathematics and computer science with proof assistants; and “Proof Pearls” (elegant, concise, and instructive examples). Important Dates: ++++++++++++++++ Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a URL where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). ============================ ========================== **Abstract Deadline:** Friday, June 7, 2013 **Submission Deadline:** Friday, June 14, 2013 **Author Notification:** Monday, August 26, 2013 **Camera-ready Papers Due:** Monday, September 16, 2013 ============================ ========================== Submission Instructions: ++++++++++++++++++++++++ Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2013 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag’s Lecture Notes in Computer Science series. Submission instructions including LaTeX style files are available from the CPP 2013 website. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. *Papers not conforming to the above requirements concerning format and length may be rejected without further consideration.* The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. Organisation ++++++++++++ :Program Co-Chairs: Georges Gonthier (Microsoft Research Cambridge) &amp; Michael Norrish (NICTA) :General Chair: Peter Schachte, *University of Melbourne* :Website: http://cpp2013.forge.nicta.com.au Program Committee ^^^^^^^^^^^^^^^^^ ========================= ======================================= Derek Dreyer MPI-SWS William Farmer McMaster University Jean-Christophe Filliâtre INRIA Cédric Fournet Microsoft Research Cambridge Benjamin Grégoire INRIA Reiner Hähnle Technische Universität Darmstadt Aquinas Hobor National University of Singapore Gyesik Lee Hankyong National University Cesar Muñoz NASA Langley Toby Murray NICTA Gopalan Nadathur University of Minnesota Claudio Sacerdoti Coen University of Bologna Peter Sewell University of Cambridge Bas Spitters University of Nijmegen Gang Tan Lehigh University Alwen Tiu Australian National University Yih-Kuen Tsay National Taiwan University Lihong Zhi Academia Sinica ========================= ======================================= ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Michael Norrish 2013-05-10T06:46:48 http://comments.gmane.org/gmane.comp.mathematics.hol/2690 <pre>(* Apologies for multiple copies *) ------------------------------------------------------------------- FINAL CALL FOR PAPERS ------------------------------------------------------------------- The 5th International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2013) Part of CICM-2013, at University of Bath, UK 8-12th of July 2013 ------------------------------------------------------------------- Important Dates --------------- * Paper submission: *Mon May 27 2013* * Notification of acceptance: Mon June 10 2013 * Camera ready copy due: Mon June 17 2013 Invited Speakers ----------------- * Conor McBride, University of Strathclyde * Gilles Dowek, INRIA * Edwin Brady, University of St Andrews * Serge Mechveliani, Russian Academy of Science Program Committee ----------------- * David Aspinall, University of Edinburgh, UK * Serge Autexier, DKFI Bremen, Germany * Jacques Carette, McMaster University, Canada * Claudio Sacerdoti Coen, University of Bologna, Italy * Gudmund Grov, Heriot Watt University, UK * Cezar Ionescu, Potsdam Institute, Germany * Ewen Maclean, University of Edinburgh, UK * Florian Rabe (co-chair), Jacobs University, Germany * Tim Sheard, Portland State University, USA * Sergei Soloviev, IRIT, France * Stephen Watt, University of Western Ontario, Canada * Makarius Wenzel, Université Paris-Sud, France * Iain Whiteside (co-chair), University of Newcastle, UK * Freek Wiedijk, Radboud University, Netherlands * Wolfgang Windsteiger, RISC, Austria PLMMS Scope ----------- The program committee welcomes submissions on programming language issues related to all aspects of mechanised mathematics systems (MMS). In particular: - Mathematical algorithms - Tactics and proof search - Proofs - Mathematical notation Of particular interest are the dimensions of: - Expressiveness - Efficiency - Correctness - Understandability and Usability - Modularity and Extensibility - Design and implementation Mechanised mathematics systems, whether stand-alone or embedded in larger systems, include but are not limited to: - Dependent typed programming languages - Proof assistants - Computer algebra systems - Proof planning systems - Theorem proving systems - Theory formation systems These issues have a very colourful history. Why are all the languages of mainstream computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical computer algebra systems? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modelling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers when using more mainstream languages for computer algebra systems, proof assistants or theorems provers? Many programming language innovations appeared in either computer algebra or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in the design of MMS that may be relevant to future programming languages, or conversely novel programming language principles that improve upon the implementation and deployment of MMS. Submission Details ------------------ Papers should be submitted via the PLMMS 2013 easychair website: https://www.easychair.org/conferences/?conf=plmms2013 Submissions must describe original unpublished work which is not been submitted for publication elsewhere. At least one author of each accepted paper is expected to attend PLMMS 2013 and present her or his paper. We wish to be flexible with paper length and will accept papers between 4 and 15 pages in length, submitted in PDF format. We invite submissions of both work-in-progress and fully polished research. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series. The corresponding style files can be downloaded from: http://www.springer.com/computer/lncs/lncs+authors Papers will be reviewed by at least three reviewers. Informal workshop proceeding will be circulated as a technical report and on CEUR-WS. Links ----- * https://www.easychair.org/conferences/?conf=plmms2013 abstract and paper submission webpage * http://www.springer.com/computer/lncs/lncs+authors submission style guide * http://www.cicm-conference.org/2013/cicm.php?event=plmms&amp;menu=general the PLMMS 2013 web site * http://www.cicm-conference.org/2013/cicm.php the CICM 2013 conference web siteThe University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Iain Whiteside 2013-05-09T10:34:50 http://comments.gmane.org/gmane.comp.mathematics.hol/2687 <pre>Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: &amp;lt;mailto:memocode-unsubscribe&lt; at &gt;lists.cs.columbia.edu&gt; CALL FOR PAPERS - MEMOCODE 2013 (NOTE: NEW EXTENDED DATES for PAPERS and DESIGN CONTEST) Eleventh ACM/IEEE International Conference on Formal Methods and Models for Codesign http://www.memocode-conference.com 18-20 October 2013, Portland, Oregon, USA Co-located with DIFTS and FMCAD SCOPE The eleventh ACM/IEEE MEMOCODE conference focuses on research and developments in methods, tools, and architectures for the design of hardware/software systems. MEMOCODE seeks submissions that present novel formal methods and design techniques to create, refine, and verify complex hardware/software systems and to tackle the tight constraints on timing, power, costs, reliability and security that these systems face. We also invite application-oriented papers, and especially encourage submissions that highlight the tools and design perspective of formal methods and models, including success as well as failure stories, constructive analysis thereof, and demonstrations of hardware/software codesign. Techniques may range from formal verification to simulation-based verification technologies, and from languages to design paradigms that unify hardware and software codesign. Architectures may range from cloud computing and multi-core platforms to networks on chip. Applications and demonstrators may address values ranging from productivity and reuse to performance and quality. MEMOCODE 2013 is co-located with FMCAD, the thirteenth conference on Formal Methods in Computer-Aided Design, and DIFTS, the International Workshop on Design and Implementation of Formal Tools and Systems. PAPER SUBMISSIONS Paper submissions must be accepted through the EasyChair review system on our web site. Papers must be 10 pages or less, and must be formatted following IEEE Computer Society guidelines. Submissions must be written in English, describe original work, and not substantially overlap papers that have been published or are being submitted to a journal or another conference with published proceedings. (NOTE: NEW, EXTENDED DATES !!!) Abstract submission deadline: May 15 Paper submission deadline: May 22 Notification of acceptance: June 18 Final version for Papers: July 17 DESIGN CONTEST MEMOCODE 2013 is proud to organize its traditional Design Contest. The conference will sponsor at least one prize with a significant monetary award. Each team delivering a complete and working solution will be invited to prepare a 2-page abstract to be published in the proceedings and to present it during a dedicated poster session at the conference. The winning teams may contribute a 4-page short paper for presentation in the conference program. Further information will be made available on our website. (NOTE: NEW, EXTENDED DATES !!!) Design Contest start: June 1 Design submission deadline: July 1 Notification of design results: July 19 Final version for abstracts: July 31 PUBLICATION Conference proceedings will be published by the IEEE Computer Society. Besides conference proceedings, we are planning a special journal issue with the very best 2013 papers of MEMOCODE, DIFTS, and FMCAD. We look forward to your participation! Marly Roncken, Jean-Pierre Talpin, and Eriko Nurvitadhi MEMOCODE 2103 Program Chairs and Design Contest Chair _______________________________________________ Memocode mailing list Memocode&lt; at &gt;lists.cs.columbia.edu------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Marly Roncken 2013-05-06T22:25:05 http://comments.gmane.org/gmane.comp.mathematics.hol/2686 <pre>Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: &amp;lt;mailto:memocode-unsubscribe&lt; at &gt;lists.cs.columbia.edu&gt; Hi all, I would like to let you know that the MEMOCODE Design Contest for this year is coming up soon, on May 15. More details are available at http://memocode.irisa.fr/2013/competition.html Looking forward to your participation! Regards, Eriko Nurvitadhi Design Contest Chair _______________________________________________ Memocode mailing list Memocode&lt; at &gt;lists.cs.columbia.edu------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Nurvitadhi, Eriko 2013-05-06T13:38:49 http://comments.gmane.org/gmane.comp.mathematics.hol/2685 <pre>FMCAD 2013 - FORMAL METHODS IN COMPUTER-AIDED DESIGN FINAL CALL FOR PAPERS International Conference on Formal Methods in Computer-Aided Design http://www.fmcad.org/FMCAD13 Portland, OR, USA October 20-23, 2013 IMPORTANT DATES Abstract Submission: May 8 Paper Submission: May 15 Author Notification: July 17 Final Version: August 14 Conference: October 20 - 23 Student Forum: (NEW! --- See below for details) Submission Deadline: June 2 Notification: August 4 KEYNOTES - Pranav Ashar, Chief Technology Officer, Real Intent, "Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC" - Lori A. Clarke, Professor, University of Massachusetts, Amherst, "Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare" TUTORIALS - Rajeev Alur, University of Pennsylvania, "Computer Augmented Program Engineering" - Jim Grundy, Intel Corporation, "Firmware Validation: Challenges and Opportunities" - Somesh Jha, Bill Harris, Tom Reps, University of Wisconsin-Madison, "Secure Programs via Game-Based Synthesis" - Other Tutorials TBD CONFERENCE SCOPE FMCAD 2013 is the thirteenth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing novel methods, technologies, theoretical results, and tools for formal reasoning about computing systems, as well as open challenges therein. FMCAD 2013 will be held in Portland, OR, USA, and co-located with MEMOCODE, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, and DIFTS 2013, the International Workshop on Design and Implementation of Formal Tools and Systems. DIFTS will be held on October 19. MEMOCODE will take place from October 18 to 19, followed by a joint FMCAD/MEMOCODE tutorial day on October 20. FMCAD will continue from October 21 to 23, 2013. TOPICS OF INTEREST FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods technology and its application to computer-aided design. Topics of interest include, but are not limited to, the following: - Advances in model checking, theorem proving, equivalence checking, abstraction and reduction techniques, compositional methods, automatic decision procedures at the bit- and word-level, probabilistic methods, and combinations of deductive methods and decision procedures. - Topics related to the application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software. This includes timing and power modeling, and verification of computing systems on all levels of abstraction. System-level design and verification, especially for embedded systems, HW/SW co-design and verification, and transaction-level verification. - Modeling and specification languages, formal semantics of known languages or their subsets, model-based design, design derivation and transformation, and correct-by-construction methods. - Experience with the application of formal and semi-formal methods to industrial-scale designs. Tools that represent formal verification enablement, new features, or a substantial improvement in the automation of formal methods. - Application of formal methods in new areas. SUBMISSIONS Submissions must be made electronically in PDF format via EasyChair. More details are available from the FMCAD Web site. The proceedings will be freely available from the FMCAD Web site. Two categories of papers can be submitted: regular papers (8 pages), containing original research; and short papers (4 pages), containing emerging results, practical experiences or original ideas that can be described succinctly. Regular and short papers must use the IEEE Transactions format on letter-size paper with a 10-point font size, see http://www.ieee.org/portal/pages/pubs/transactions/stylesheets.html. We recommend that self-citations be written in the third person. Submissions must contain original research that has not been previously published, nor concurrently submitted for publication. Any partial overlap with any published or concurrently submitted paper must be clearly indicated. If experimental results are reported, authors are strongly encouraged to provide adequate access to their data so that results can be independently verified. A small number of accepted papers will be considered for a distinguished paper award. PUBLICATION Accepted papers, both regular and short, will be published in the FMCAD Conference Proceedings. We expect to have ACM In-Cooperation Status and IEEE Technical Co-Sponsorship, as has been the case with previous FMCAD conferences. FMCAD and authors will share the copyright for accepted papers and we plan on publishing the proceedings in the ACM Digital Library and in IEEE Xplore. As with recent editions of FMCAD, the papers are also expected to be available online from the FMCAD Web page. In addition, we are planning a special journal issue with the best papers of FMCAD, DIFTS, and MEMOCODE 2013. STUDENT FORUM FMCAD 2013 will host a Student Forum that provides a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community, and solicit feedback. Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. The event will consist of short presentations by the student authors of each accepted submission, and of a poster that will be on display throughout the duration of the conference. Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their poster and presentation to the FMCAD webpage. Limited funds will be available for travel assistance for students with accepted contributions. CO-LOCATED EVENTS The following meetings will be co-located with this year's edition: - MEMOCODE 2013, the ACM/IEEE International Conference on Formal Methods and Models for Codesign (http://www.memocode-conference.com). - DIFTS 2013, International Workshop on Design and Implementation of Formal Tools and Systems We are also proud to host this year's Hardware Model Checking Competition (HWMCCC 2013). ORGANIZING COMMITTEE CHAIRS Barbara Jobstmann, Jasper Design Automation and CNRS-VERIMAG Sandip Ray, Intel Corporation LOCAL ARRANGEMENT CHAIR Joe Leslie-Hurd, Intel Corporation PUBLICATION CHAIR Julien Schmaltz, Open University of The Netherlands TUTORIAL CHAIR Malay Ganai, NEC Laboratories America STUDENT FORUM CHAIR Thomas Wahl, Northeastern University PUBLICITY CHAIR Chao Yan, Intel Corporation WEBMASTER Shilpi Goel, University of Texas at Austin PROGRAM COMMITTEE Jason Baumgartner, IBM Corporation Dirk Beyer, University of Passau Armin Biere, Johannes Kepler University Per Bjesse, Synopsys Nikolaj Bjorner, Microsoft Research Roderick Bloem, TU Graz Gianpiero Cabodi, Politecnico di Torino Hana Chockler, IBM Research Alessandro Cimatti, FBK-irst Koen Claessen, Chalmers University of Technology Malay Ganai, NEC Labs America Steven German, IBM Ganesh Gopalakrishnan, University of Utah Alberto Griggio, FBK-IRST Ziyad Hanna, University of Oxford Keijo Heljanko, Aalto University Alan Hu, University of British Columbia William Hung, Synopsys Inc Warren Hunt, University of Texas Susmit Jha, Strategic CAD Lab, Intel Shuvendu Lahiri, Microsoft Research Panagiotis Manolios, Northeastern University Tom Melham, University of Oxford John O'Leary, Intel Corporation Lee Pike, Galois, Inc. Ruzica Piskac, Max Planck Institute for Software Systems (MPI-SWS) Philipp Ruemmer, Uppsala University, Department of Information Technology Cesar Sanchez, IMDEA Software Institute Julien Schmaltz, Open University of The Netherlands Natasha Sharygina, University of Lugano, Switzerland Anna Slobodova, Centaur Technology Niklas Sorensson, Mentor Graphics Daryl Stewart, ARM Thomas Wahl, Northeastern University Georg Weissenbacher, Vienna University of Technology STEERING COMMITTEE Jason Baumgartner, IBM, USA Armin Biere, Johannes Kepler University in Linz, Austria Aarti Gupta, NEC Labs America, USA Warren Hunt, University of Texas at Austin, USA Panagiotis Manolios, Northeastern University, USA ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may </pre> Chao Yan 2013-05-07T03:18:43 http://comments.gmane.org/gmane.comp.mathematics.hol/2680 <pre>Apologies for multiple copies of this email. ************************************************************************ *** DIFTS'13 DESIGN and IMPLEMENTATION of FORMAL TOOLS and SYSTEMS CALL FOR PAPERS ************************************************************************ *** Second International Workshop on Design and Implementation of Formal Tools and Systems (co-located with FMCAD and MEMOCODE 2013) http://www.cmpe.boun.edu.tr/difts13/ Portland, OR, USA October 19, 2013 IMPORTANT DATES Paper submission: July 24, 2013 Author notification: August 24, 2014 WORKSHOP SCOPE DIFTS (Design and Implementation of Formal Tools and Systems) workshop emphasizes insightful experiences in formal tools and systems design. The first DIFTS workshop was held in 2011. It provides a forum for sharing challenges and solutions that are original with ground breaking results. Often the design and implementation of tools for formal analysis require non-trivial engineering decisions. Many challenges are faced, which often can only be met with ingenious implementation techniques. These techniques actually play a crucial role in making the idea work in practice. The workshop provides an opportunity for discussing engineering aspects and various design decisions required to put such formal tools and systems into practical use. TOPICS OF INTEREST DIFTS takes a broad view of the formal tools/systems area, and solicits contributions from domains including, but not restricted to, decision procedures, verification, testing, validation, diagnosis, debugging, and synthesis. This workshop encourages and appreciates system development activities, and facilitates transparency in the experimentation. It will also serve as a platform to discuss open problems and future challenges in practicing formal methods. SUBMISSION The workshop specifically solicits contributions with substantial engineering details that often do not get published but has significant practical impact. Papers in the following two categories are solicited: (a) system category (10 pages, double column, 11pt), and (b) tool category (8 pages, double column, 11pt). In the system category, we invite papers that have original ideas accompanied with novel integration techniques, adequate design/implementation details, important design choices made and explored, and good experimental results. In the tool category, we invite papers that focus primarily on the engineering aspects of some known/popular algorithm, with significant emphasis on the design/implementation details, and various design choices made to advance current state-of-the-art approaches. The page limit for submissions in the system category is 10 pages in double column format and for submissions in the tool category is 8 pages in double column format. Submission of papers should be made electronically in PDF format via EasyChair. More details will be provided on the DIFTS web site. EVALUATION To keep maintain uniformity and fairness in the reviewing process, the program committee will evaluate the technical contribution of each submission based on the following guidelines: the paper should provide enough details for others to reproduce the results; and should solve a clearly-stated problem that is significant and has wide interest; and the paper should provide enough motivation for the design choices made. Overall, the paper should also clearly identify what the main contributions of the work are. PUBLICATION All accepted contributions will be included in informal proceedings. High quality submissions will be considered for a special issue of journals such as FMSD (Formal Methods in System Design) or IEEE TC (Transactions on Computers). ORGANIZATION PROGRAM CHAIRS Malay K. Ganai, NEC Labs America, USA Alper Sen, Bogazici University, Turkey PROGRAM COMMITTEE Armin Biere, Johannes Kelpler University, Austria Gianpiero Cabodi, Politecnico di Torino, Italy Franco Fummi, University of Verona, Italy Malay K. Ganai, NEC Labs America, USA Daniel Grosse, University of Bremen, Germany William Hung, Synopsys Inc., USA Daniel Kroening, Oxford University, UK Alper Sen, Bogazici University, Turkey Ofer Strichman, Technion - Israel Institute of Technology, Israel Chao Wang, Virginia Tech, USA ------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite It's a free troubleshooting tool designed for production Get down to code-level detail for bottlenecks, with &lt;2% overhead. Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap2_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Malay Ganai 2013-05-02T17:13:01 http://comments.gmane.org/gmane.comp.mathematics.hol/2679 <pre>********************************************************** CALL FOR PAPERS ********************************************************** VeriSure: Verification and Assurance In association with Computer-Aided Verification (CAV) 2013 July 14, 2013, Saint Petersburg, Russia http://fm.csl.sri.com/VeriSure/ Workshop Organizers Sam Owre, Natarajan Shankar, and John Rushby, SRI International *** Workshop Description *** The purpose of this workshop is to explore issues at the conjunction of computer-aided verification and system assurance. An autonomous car, for example, must safely negotiate an environment that is imperfectly and incompletely modeled, while using actuators that are themselves imperfect, and guided by fallible sensors whose data requires delicate interpretation and fusion. Assurance here clearly requires more than verification, but can build on verified foundations. In general, computer-aided verification is usually performed in support of a larger activity whose goal is to provide assurance for a decision with large consequences. The decision may be to send a hardware design for fabrication or to release a commercial software product, in which cases the consequences are economic, or it may be to deploy a system in a context with potential consequences for societal safety or security. In all these cases, verification will be just one of many strands of evidence that contribute to system assurance, and the overall structure of the assurance may be specified or constrained by regulation or certification requirements. This workshop will explore challenges and opportunities posed for computer-aided verification by the larger context of system assurance. One immediate set of challenges arises from the (recursive) need to provide assurance for the claims delivered by computer-aided verification itself. Related is the challenge of providing assurance for the assumptions and requirements with respect to which the verification is performed. These challenges are situated in pragmatic engineering settings where choices must be made about what should be verified, and to what level of detail, and what should or must be assured by other means (such as testing, human review, or runtime monitoring), and how all these should be combined. Opportunities arise from the possibility of formalizing and verifying aspects of the larger assurance activity, stimulated by recent proposals that this should be structured as an assurance "case." An assurance case is composed of claims, argument, and evidence, where the argument justifies claims (e.g., for security or safety) based on evidence about the system and its development. An interesting complication is that many top-level claims are probabilistic (e.g., 10-9 for certain aircraft software) while traditional formal verification is unconditional. We solicit papers on relevant topics, which include but are not restricted to the following. We encourage exploratory work that will stimulate discussion. o Quantitative and qualitative assurance claims and arguments o Integration of formal verification with assurance and with assurance cases o Modular and incremental methods of verification and assurance o Toolchains for integrated assurance arguments o Soundness guarantees for tools, toolchains, and workflows o Certification and regulatory requirements and standards o Experience reports and challenges The program will include invited speakers, presentation of selected papers, and discussion. The workshop is colocated with CAV 2013 in Saint Petersburg, Russia *** Invited Speakers *** Robin Bloomfield, City University and Adelard Others to be announced *** Workshop Committee *** Jean-Christophe Filliâtre, LRI Université Paris Sud, France Mike Gordon, Cambridge University, UK Sofia Guerra, Adelard, UK Michael Holloway, NASA Langley, USA Michaela Huhn, TU-Clausthal, Germany Florent Kirchner, CEA, France Gerwin Klein, NICTA, Australia Tom Maibaum, McMaster University, Canada Bertrand Meyer, ETH Zurich, Switzerland Grigori Mints, Stanford University, USA Harald Ruess, FORTISS, Germany Oleg Sokolsky, University of Pennsylvania, USA Virginie Wiels, ONERA, France *** Important Dates *** Position papers due May 3 Reviews/decisions June 2 Camera ready versions due June 28 VeriSure Workshop July 14 Note: We ask potential participants to apply for a visa invitation letter as soon as possible (even if their trip plans may change later). For further details please check the CAV Visa page at http://cav2013.forsyte.at/visa/ *** Electronic Submissions *** Submissions should be in PDF format between 3-12 pages. We recommend the guidelines for ACM SIG Proceedings. The submissions page is open at https://www.easychair.org/conferences/?conf=verisure2013 ------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite It's a free troubleshooting tool designed for production Get down to code-level detail for bottlenecks, with &lt;2% overhead. Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap2 _______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Sam Owre 2013-05-03T07:23:43 http://comments.gmane.org/gmane.comp.mathematics.hol/2678 <pre>MCS Special Issue: Formal Proofs for Mathematics and Computer Science &lt;http://www-sop.inria.fr/marelle/MCS-FP-2013/&gt; CALL FOR PAPERS We invite submission of papers on Proof Formalization for possible publication in this Mathematics in Computer Science (MCS) special issue. Deadlines: Deadline for paper submission: August 31, 2013 Notification of acceptance/rejection: December 15, 2013 Publication of the special issue: Early 2014 Scope: In recent years, the use of Interactive Theorem Provers for the formalization of mathematical proofs has seen impressive advances: - In mathematics, the Flyspeck project and the formal verification of Feit-Thompson theorem indicate that formal proofs may play an active role in the development of new mathematics. - In computer science, the CompCert and L4.verified projects indicate that non-trivial systems like compilers and operating systems can be fully verified. Still, much more progress is needed in order to make the use of this new technology ubiquitous. The aim of this special issue is to bring together high quality contributions which present recent advances in the use of formal proofs and new perspectives on the technology of interactive theorem proving. Submission guidelines: Papers should be submitted as a pdf. While there is no strict page limit, papers are expected to be approximately 20 pages long. The LaTeX "mathincs" class should be used, according to the guidelines at &lt;http://www.springer.com/birkhauser/mathematics/journal/11786&gt;. Papers should either be accompanied by a formalization, a library for an interactive theorem prover, or an implemented system. Submission is preferably through EasyChair at &lt;https://www.easychair.org/conferences/?conf=mcsfp2013&gt;. Editors of the Special Issue: Laurent Théry, INRIA Sophia Antipolis email:&lt;Laurent.Thery&lt; at &gt;inria.fr&gt; Freek Wiedijk, Radboud University Nijmegen email:&lt;freek&lt; at &gt;cs.ru.nl&gt; ------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite It's a free troubleshooting tool designed for production Get down to code-level detail for bottlenecks, with &lt;2% overhead. Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap2 </pre> Laurent Théry 2013-05-05T23:49:51 http://comments.gmane.org/gmane.comp.mathematics.hol/2669 <pre> CALL FOR PARTICIPATION Fifth Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013) May 17--19, 2013, Atherton, California https://sites.google.com/site/vstte2013/ The Fifth IFIP Working Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich in 2005 followed by conferences in Toronto (2008), Edinburgh (2010), and Philadelphia (2012). The goal of this conference is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. Registration: http://fm.csl.sri.com/VSTTE2013/registration.html Note that the Summer School on Formal Techniques follows shortly after at the same location (http://fm.csl.sri.com/SSFT13/) Program: -------- Thur May 16, 2013 6PM: Wine/Cheese Reception Fri May 17, 2013 9-10AM: Alex Aiken (Stanford): Using Learning Techniques in Invariant Inference Abstract: Arguably the hardest problem in automatic program verification is designing appropriate techniques for discovering loop invariants (or, more generally, recursive procedures). Certainly, if invariants are known, the rest of the verification problem becomes easier. This talk presents a family of invariant inference techniques based on using test cases to generate an underapproximation of program behavior and then using learning algorithms to generalize the underapproximation to an invariant. These techniques are simpler, much more efficient, and appear to be more robust than previous approaches to the problem. If time permits, some open problems will also be discussed. 10-10.30AM: Break 10.30-12 noon: Static Analysis Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak. Classifying and Solving Horn Clauses for Verification Olivier Bouissou, Eric Goubault, Sylvie Putot, Jean Goubault-Larrecq and Assale Adje. Static Analysis of Programs with Imprecise Probabilistic Inputs Etienne Kneuss, Viktor Kuncak and Philippe Suter. Effect Analysis for Programs with Callbacks noon-1.30PM: Lunch 1.30-3PM: Model Checking Pamela Zave and Jennifer Rexford. Compositional Network Mobility Nicolas Rosner, Carlos Gustavo Lopez Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili and Marcelo Frias. Parallel Bounded Verification of Alloy Models by TranScoping Stephan Falke, Florian Merz and Carsten Sinz. Extending the Theory of Arrays: memset, memcpy, and Beyond 3-3.30PM: Break 3.30-4.30PM: Unrolling Tuan-Hung Pham and Michael Whalen. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types Julian Tschannen, Carlo A. Furia, Martin Nordio and Bertrand Meyer. Program Checking With Less Hassle 5-6PM: Panel (TBD) Sat May 18, 2013 9-10AM: Nikhil Swamy (Microsoft Research): F*: Certified Correctness for Higher-order Stateful Programs Abstract: F* is an ML-like programming language being developed at Microsoft Research. It has a type system based on dependent types and a typechecker that makes use of an SMT solver to discharge proof obligations. The type system is expressive enough to express functional correctness properties of typical, higher-order stateful programs. We have used F* in a variety of settings, including in the verification of security protocol implementations; as a source language for secure web-browser extensions; as an intermediate verification language for JavaScript code; to verify the correctness of compilers; as a relational logic for probabilistic programs; and as a proof assistant in which to carry out programming language metatheory. We have also used F* to program the core typechecker of F* itself and have verified that it is correct. By bootstrapping this process using the Coq proof assistant, we obtain a theorem that guarantees the existence of a proof certificate for typechecked programs. I will present a brief overview of the F* project, drawing on the examples just mentioned to illustrate the features of the F* language and certification system. For more about F*, visit http://research.microsoft.com/fstar. 10-10.30: Break 10.30-12: Reasoning Methodology K. Rustan M. Leino and Nadia Polikarpova. Verified Calculations Jean-Christophe Filliatre, Claude Marché, François Bobot, Andrei Paskevich and Guillaume Melquiond. Preserving User Proofs Across Specification Changes Daniel Jost and Alexander J. Summers. An automatic encoding of VeriFast Predicates into Implicit Dynamic Frames 12-1.30: Lunch 1.30-2.30: Andre Platzer: How to Explain Cyber-Physical Systems to Your Verifier Abstract: Despite the theoretical undecidability of program verification, practical verification tools have made impressive advances. How can we take verification to the next level and use it to verify programs in cyber-physical systems (CPSs), which combine computer programs with the dynamics of physical processes. Cars, aircraft, and robots are prime examples where this matters, because they move physically in space in a way that is determined by discrete computerized control algorithms. Because of their direct impact on humans, verification for CPSs is even more important than it already is for programs. This talk describes how formal verification can be lifted to one of the most prominent models of CPS called hybrid systems, i.e. systems with interacting discrete and continuous dynamics. It presents the theoretical and practical foundations of hybrid systems verification. The talk shows a systematic approach that is based on differential dynamic logic comes with a compositional proof technique for hybrid systems and differential equations. This approach is implemented in the verification tool KeYmaera and has been used successfully for verifying properties of aircraft, railway, car control, autonomous robotics, and surgical robotics applications. 2.30-3PM: Break 3-5.00PM: System Verification Shilpi Goel and Warren Hunt. Automated Code Proofs on a Formal Model of the X86 Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein. seL4: from General Purpose to a Proof of Information Flow Enforcement Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif. Verification of a Virtual Filesystem Switch Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Yu Liu. Verifying Chinese Train Control System Under a Combined Scenario by Theorem Proving 5.30-6.30PM: Panel (TBD) 8PM: Banquet 9-10AM: Sandrine Blazy A Tutorial on the CompCert Verified Compiler. 10-10.30: Break 10.30-noon: Verified Tools Sandrine Blazy, André Maroneze and David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis Frédéric Besson, Pierre-Emmanuel Cornilleau and Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers Anthony Narkawicz and Cesar Munoz. A Formally Verified Generic Branching Algorithm for Global Optimization noon-1.30: Lunch 1.30-5: Excursion ------------------------------------------------------------------------------ Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET Get 100% visibility into your production application - at no cost. Code-level diagnostics for performance bottlenecks with &lt;2% overhead Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap1 _______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Sam Owre 2013-05-02T03:32:18 http://comments.gmane.org/gmane.comp.mathematics.hol/2668 <pre>Third Summer School on Formal Techniques May 20 - May 24, 2013 Menlo College, Atherton, CA http://fm.csl.sri.com/SSFT13 Follows VSTTE May 17-19 in the same location: https://sites.google.com/site/vstte2013/ Formal verification techniques such as model checking, satisfiability, and static analysis have matured rapidly in recent years. This school, the third in the series, will focus on the principles and practice of formal verification, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in using verification technology in their own research in computing as well as engineering, biology, and mathematics. Students at the school will have the opportunity to experiment with the tools and techniques presented in the lectures. The first Summer Formal school (SSFT11; http://fm.csl.sri.com/SSFT11) was held in May 2011 and the second (SSFT12; http://fm.csl.sri.com/SSFT12) was held in May 2012. We have NSF support for the travel and accommodation for students from US universities, but welcome applications from graduate students at non-US universities as well. Non-US students will have to cover their travel and lodging expenses (around $500). The deadline for applications is April 30. Non-US students requiring US visas are requested to apply early (by April 15). Interested students can submit their application at http://fm.csl.sri.com/SSFT13 The lectures at the school include: ================================================================== Title: Decision Methods for Arithmetic Lecturer: Leonardo de Moura, Microsoft Research Abstract: Decision methods for arithmetic are extensively used in the formal verification and analysis of software and cyber-physical systems, computer algebra, and formalized mathematics. In these talks, we will cover several decision methods for fragments of arithmetic such as the elementary theories of algebra and geometry over the Real and Complex numbers. We will also describe the general techniques used in the design of these procedures: saturation, model-based methods, abstract/refine loop, infinitesimals, etc. We assume only a basic grounding in first-order logic. ================================================================== Title: Advanced Theorem Proving Techniques in PVS with Applications Lecturer: Cesar Munoz, NASA Langley Research Center Hampton, VA 23681-2199, USA Abstract: The Prototype Verification System (PVS) [http://pvs.csl.sri.com&lt;http://pvs.csl.sri.com/&gt;] is an interactive environment for the specification and verification of systems. PVS provides a strongly typed specification language, which is based on Higher-Order Logic. The type system of PVS supports: sub-typing, dependent-types, abstract data types, parametric types, records, unions, and tuples. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This seminar will provide a gentle introduction to advanced PVS features, including types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. ================================================================== Title: Static and Dynamic Verification of Concurrent Programs Lecturer: Aarti Gupta, NEC Labs Abstract: The need to harness the computing power of modern multi-core platforms has driven a resurgence of interest in concurrent programs. However, it is very challenging to develop correct concurrent programs, and in practice programs often exhibit bugs related to subtle synchronization effects. These lectures will describe various static and dynamic techniques underlying automatic verification and debugging of concurrent programs. The emphasis will be on main ideas to reason about synchronizations and interleavings between interacting threads or processes. On the static side, we first review some theoretical results on model checking based on interacting pushdown system (PDS) models. Decidability results here limit the patterns of synchronization allowed. Next, we consider the practice of model checking concurrent programs, where the main challenge is in managing the explosion in interleavings. We consider both explicit and symbolic state space exploration, where various techniques are inspired by successful verification of finite state systems on one hand, and sequential programs on the other. Due to scalability limitations of static verification, there has been increased interest in dynamic techniques for systematically exploring (parts of) concurrent programs. We discuss preemptive context bounding techniques that control the scheduler to dynamically explore other interleavings. We also consider predictive analysis techniques, where a trace-based model derived from dynamic executions is used to predict concurrency bugs. ================================================================== Title: Program verification and synthesis as Horn-like constraint solving Lecturer: Andrey Rybalchenko, TU Munich Abstract: First, we review how proving reachability and termination properties of transition systems, procedural programs, multi-threaded programs, and higher- order functional programs can be reduced to constraint solving for Horn-like constraints. This step will cover properties over program variables of scalar and array data types. Second, we show how universal and existential temporal properties can be proved using contraint-based setting equipped with existential quantification. Third, we present a reduction from reactive program synthesis to existentially quantified Horn-like constraints. Finally, we discuss adequate solving algorithms and tools. The material would cover/export syntax and semantics of Horn clauses over theory literals, basics of temporal proof rules for reasoning about programs, basics of CTL and synthesis together with deductive proof rules, bottom-up inference/ resolution of Horn clauses, Skolemization, abstraction, interpolation. ================================================================== Title: Verified Programming with VCC Speaker: Ernie Cohen Abstract: In the last few years it has become practical to write real-world code and prove that it meets its specifications. This course provides an introduction to the joys of verified programming using VCC, a deductive verifier for concurrent C code. ================================================================== Title: Speaking Logic Speaker: Natarajan Shankar, SRI International Abstract: Formal logic has become the lingua franca of computing. It is used for specifying digital systems, annotating programs with assertions, defining the semantics of programming languages, and proving or refuting claims about software or hardware systems. Familiarity with the language and methods of logic is a foundation for research into formal aspects of computing. This course covers the basics of logic focusing on the use of logic as a medium for formalization and proof. --- To opt-out from this mailing list, send an email to fm-announcements-request&lt; at &gt;lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner&lt; at &gt;lists.nasa.gov ------------------------------------------------------------------------------ Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET Get 100% visibility into your production application - at no cost. Code-level diagnostics for performance bottlenecks with &lt;2% overhead Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap1_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGTInc.)] 2013-05-01T14:55:55 http://comments.gmane.org/gmane.comp.mathematics.hol/2667 <pre> Apologies for multiple postings. VSTTE 2013 will be held in Bay Area following NFM 2013 (http://ti.arc.nasa.gov/events/nfm-2013/) ============================================================================== CALL FOR PARTICIPATION Fifth Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013) May 17--19, 2013, Menlo College, Atherton, California [https://sites.google.com/site/vstte2013/] The Fifth IFIP Working Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich in 2005 followed by conferences in Toronto (2008), Edinburgh (2010), and Philadelphia (2012). The goal of this conference is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. Invited speakers: Alex Aiken (Stanford), Sandrine Blazy (Rennes), Nikhil Swamy (Microsoft), Andre Platzer (CMU) Accepted papers: Daniel Jost and Alexander J. Summers. An automatic encoding of VeriFast Predicates into Implicit Dynamic Frames Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak. Classifying and Solving Horn Clauses for Verification Tuan-Hung Pham and Michael Whalen. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types Olivier Bouissou, Eric Goubault, Sylvie Putot, Jean Goubault-Larrecq and Assale Adje. Static Analysis of Programs with Imprecise Probabilistic Inputs Etienne Kneuss, Viktor Kuncak and Philippe Suter. Effect Analysis for Programs with Callbacks K. Rustan M. Leino and Nadia Polikarpova. Verified Calculations Jean-Christophe Filliatre, Claude Marché, François Bobot, Andrei Paskevich and Guillaume Melquiond. Preserving User Proofs Across Specification Changes Pamela Zave and Jennifer Rexford. Compositional Network Mobility Julian Tschannen, Carlo A. Furia, Martin Nordio and Bertrand Meyer. Program Checking With Less Hassle Nicolas Rosner, Carlos Gustavo Lopez Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili and Marcelo Frias. Parallel Bounded Verification of Alloy Models by TranScoping Stephan Falke, Florian Merz and Carsten Sinz. Extending the Theory of Arrays: memset, memcpy, and Beyond Sandrine Blazy, André Maroneze and David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis Frédéric Besson, Pierre-Emmanuel Cornilleau and Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers Anthony Narkawicz and Cesar Munoz. A Formally Verified Generic Branching Algorithm for Global Optimization Shilpi Goel and Warren Hunt. Automated Code Proofs on a Formal Model of the X86 Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein. seL4: from General Purpose to a Proof of Information Flow Enforcement Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif. Verification of a Virtual Filesystem Switch Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Yu Liu. Verifying Chinese Train Control System Under a Combined Scenario by Theorem Proving School/Workshops: The conference will be colocated with the Third Summer School on Formal Techniques, and is preceded by NFM 2013 at NASA Ames and followed by ICSE 2013 at San Francisco. Conference Chair: Natarajan Shankar, SRI International Program Chairs: Ernie Cohen, Microsoft, Andrey Rybalchenko, TU Munich Program Committee: Josh Berdine, Ahmed Bouajjani, Marsha Chechik, Jean-Christophe Filliatre, Silvio Ghilardi, Aarti Gupta, Arie Gurfinkel, Andrew Ireland, Ranjit Jhala, Cliff Jones, Rajeev Joshi, Gerwin Klein, Daniel Kroening, Gary Leavens, Xavier Leroy, Zhiming Liu, Pete Manolios, Tiziana Margaria, David Monniaux, Peter Mueller, David Naumann, Aditya Nori , Peter O'Hearn, Matthew Parkinson, Wolfgang Paul, Andreas Podelski, Zhang Shao, Willem Visser, Thomas Wies, Jim Woodcock, Kwangkeun Yi, Pamela Zave, Lenore Zuck Publicity Chair: Sam Owre, SRI International Steering Committee: Tony Hoare, Andrew Ireland, Jay Misra, Natarajan Shankar, Jim Woodcock --- To opt-out from this mailing list, send an email to fm-announcements-request&lt; at &gt;lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner&lt; at &gt;lists.nasa.gov ------------------------------------------------------------------------------ Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET Get 100% visibility into your production application - at no cost. Code-level diagnostics for performance bottlenecks with &lt;2% overhead Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap1_______________________________________________ hol-info mailing list hol-info&lt; at &gt;lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info </pre> Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGTInc.)] 2013-05-01T14:54:56 Search the mailing list at Gmane query http://search.gmane.org/?group=$group=gmane.comp.mathematics.hol