[TYPES/announce] Verification of randomized algorithms: open PhD/post doc position

and basic knowledge of the other area and will be keen to bridge the gap between them. The position will be filled as soon as possible. Please send your formal application (including the usual material and the names of two references) or informal enquiry directly to me. Best regards, Tobias

[TYPES/announce] ISABELLE WORKSHOP 2016: Call for Papers

: Tobias Nipkow, Larry Paulson and Makarius Wenzel smime.p7s Description: S/MIME Cryptographic Signature

[TYPES/announce] Marktoberdorf Summer School: Call for Participation

Verification of an ML Compiler TOBIAS NIPKOW: Verified Analysis of Functional Data Structures LARRY PAULSON: Proof Support for Hybrid System Analysis ANDRE PLATZER: Dynamic Logic for Dynamical Systems We look forward to seeing you in Marktoberdorf in August! Orna Grumberg Tobias

[TYPES/announce] Two phd/post-doc positions: FORMALIZATION AND VERIFICATION OF TRAFFIC RULES FOR AUTOMATED VEHICLES

w6.in.tum.de/en/people/prof-dr-ing-matthias-althoff) and Tobias Nipkow (http://www.in.tum.de/~nipkow/) at the Technical University Munich. It is funded by the German Research Foundation (DFG). Remuneration will be according to the German public sector salary scale TV-L E13 (starting at about 3

[TYPES/announce] [isabelle] Open position: Formal Verification Engineer (m/f/x) at HENSOLDT Cyber in Munich

[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] HENSOLDT Cyber develops embedded IT products that meet the highest security requirements. It integrates an invulnerable operating system with security-hardened hardware to build the most se

[TYPES/announce] Isabelle Users Workshop 2012

the workshop website. Submission URL: http://www.easychair.org/conferences/?conf=isabelle2012 Important Dates: * Paper submission deadline: June 15 * Notification of acceptance: June 29 * Workshop: August 12 Organisers: Tobias Nipkow, Larry Paulson and Makarius Wenzel

[TYPES/announce] Isabelle Users Workshop 2012 — final call

the workshop website. Submission URL: http://www.easychair.org/conferences/?conf=isabelle2012 Important Dates: * Paper submission deadline: June 15 * Notification of acceptance: June 29 * Workshop: August 12 Organisers: Tobias Nipkow, Larry Paulson and Makarius Wenzel

[TYPES/announce] PhD or postdoctoral position: Formalisation of Automata Theory and Model Checking

the project * the names and contact details of two referees. Enquiries and applications should be sent to Tobias Nipkow

[TYPES/announce] New Book: Concrete Semantics

[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Concrete Semantics - A Proof Assistant Approach Tobias Nipkow & Gerwin Klein http://www.in.tum.de/~nipkow/Concrete-Semantics/ We

[TYPES/announce] ISABELLE WORKSHOP and TUTORIAL

[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PARTICIPATION ISABELLE WORKSHOP and TUTORIAL http://vsl2014.at/isabelle July 13, 2

[TYPES/announce] 2-year postdoc position on security verification at TUM

intended start date is February 2015 but can be negotiated. Interested candidates should send a CV, list of publications and a brief statement of research interests to Tobias Nipkow (nipkow at in tum de) and Andrei Popescu (a.popescu at mdx ac uk). smime.p7s Description: S/MIME Cryptographic

[TYPES/announce] Now out in print: "Concrete Semantics with Isabele/HOL"

0541-3 At the same time our electronic version will remain online here: http://www.concrete-semantics.org/ Tobias Nipkow & Gerwin Klein smime.p7s Description: S/MIME Cryptographic Signature

[TYPES/announce] CfP: Isabelle Tutorial at ITP in Nanjing

[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Participation -- Isabelle Tutorial at ITP -- August 21-23, Nanjing, China This intensive 3-day tut

[TYPES/announce] New book: Functional Algorithms, Verified!

[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Functional Algorithms, Verified! http://functional-algorithms-verified.org/ This book is an introduction to data structures and algorithms for functional languages, with a focus on proofs.

[TYPES/announce] PhD Positions in Program and Model Analysis (TUM, LMU)

n Hofmann, Alexander Knapp, Alois Knoll, Tobias Nipkow, Helmut Seidl, Christian Urban, Helmut Veith and Martin Wirsing. Objective. The programme will enable PhD students to conduct leading-edge research on methods, algorithms and tools for the analysis of programs and models of information sy

[TYPES/announce] International Summer School Marktoberdorf

el Checking Sharad Malik: Boolean Satisfiability Solvers: Techniques and Extensions Tobias Nipkow: Interactive Proof: Hands-on Introduction Peter O'Hearn: Lectures on Separation Logic Andrei Sabelfeld: Information-Flow Security Helmut Seidl: Precise Fix-point Computation through Strategy Itera