[TYPES/announce] Postdoc position at CMU: Verified DSLs for high assurance systems

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are looking for a motivated postdoctoral scholar to work on formal
methods for the development of high-assurance software and cyber-physical
systems. In particular, the project involves the development and
enhancement of systems through the composition and verification of programs
written in high-level domain-specific languages (DSLs). Potential research
problems include: (1) design and implementation of DSLs for high-assurance
autonomous systems, (2) compositional verification techniques for the DSLs,
and (3) techniques for debugging and repair of DSL programs. You will also
be expected to mentor PhD students involved in this project and contribute
to the development of a scalable, practical DSL development environment.

** Location **
You will be a member of the Institute for Software Research, School of
Computer Science at Carnegie Mellon University in the USA. Pending the
evolving situation with COVID-19, you will be expected to work from
Pittsburgh, PA.

** Qualifications **
Candidates are expected to have a PhD in Computer Science or related
fields, with a strong background and research record in formal methods,
software engineering, and/or programming languages. Familiarity with
automated verification technologies (e.g., model checkers, SMT solvers) is
desirable.

** Timeline **
The position is expected to begin in September 2021 for 1 year, with a
possibility of extension.

** Instructions **
To apply, please send a copy of your latest CV and research statement to
Eunsuk Kang (esk...@cmu.edu).

[TYPES/announce] CfP: Practical Formal Verification for Software Dependability Workshop (AFFORD'19)

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CALL FOR PAPERS
===
Workshop on Practical Formal Verification for Software Dependability 
(AFFORD'19), Porto, Portugal, https://sites.google.com/site/affordworkshop 
<https://sites.google.com/site/affordworkshop>

Co-located with Formal Methods 2019 (FM'19), 7th October, 2019


IMPORTANT DATES:
===

Submission due: June 30th, 2019
Authors notification: July, 31th, 2019
Camera ready: August 15th, 2019 

===

For a large majority of software engineers and developers, formal verification 
techniques are seen rather
as expert tools and not as engineering tools that can be used on a daily basis. 
This is mostly the case in
the context of main stream systems (e.g. automotive, medical, industrial 
automation) where pragmatics
(e.g. personnel skills, cost structures, deadlines, existent processes, 
existent organization, legacy code)
plays a major role.

This workshop aims to build a community interested in the application of formal 
verification techniques
to increase dependability of software intensive systems, by developing and 
promoting approaches,
techniques and tools that can be understood and applied by practicing engineers 
– without special
education in formal methods. Specifically, we aim to bring together researchers 
and practitioners 
interested in lowering the adoption barrier to use formal verification for the 
development of dependable
software. We especially focus on the needs of main stream developers that do 
not (necessarily) work
on highly safety critical systems but on more main stream systems that still 
need to be dependable.


TOPICS OF INTEREST include but are not limited to:

- increase software dependability by using formal verification
- lowering the adoption barrier of formal verification by practicing engineers
- using formal verification results as evidence for certification
- complementing formal verification with reviews and tests
- measuring the confidence gained even when incomplete or unsound verification 
is used
- process-phase specific formal verification techniques: from requirements 
engineering to deployment and software maintenance
- integrating formal verification with agile development
- using formal verification in the development of low criticality systems
- domain specific formal verification (e.g. embedded systems, web applications)
- use of ”invisible” formal techniques like type-systems
- evaluate and increase the usability of formal verification tooling (e.g. 
specification of verification conditions, interpretation of verification 
results, specification of the environment)
- using domain specific languages and model based development to improve the 
usability of verification
- tools that provide a high degree of automation
- integration of formal techniques in development environments
- industrial experiences with using formal verification in contexts as 
described above
- experience about failures to apply suitable verification in an industrial 
context

Papers must be written in English, and be formatted according to the Springer 
LNCS format. Full papers 
must not exceed 10 pages and short papers 5 pages. Full papers should describe 
complete research 
results related to the topics of the workshop, whereas short papers can contain 
work in progress or 
novel ideas. We put special focus on the potential of the proposed approaches 
to address the needs 
of practitioners. After rigorous review, all the accepted papers will published 
by Springer in the 
FM Workshops Post-Proceedings Lecture Notes in Computer Science.

Paper submission will be done electronically through EasyChair – 
https://easychair.org/conferences/?conf=afford19 
<https://easychair.org/conferences/?conf=afford19> 

Submission implies the willingness of at least one of the authors to register 
and present the paper, if accepted. 

PROGRAM COMMITTEE:
===
- Toshiaki Aoki, JAIST, Japan
- Paolo Arcaini, NII, Japan
- Sebastian Fischmeister, University of Waterloo, Canada
- Marc Frappier, Universite de Sherbrooke, Canada
- Alessandro Fantechi, Università di Firenze, Italy
- Stefania Gnesi, ISTI, Italy
- Rajeev Joshi, Amazon Web Services, USA
- Eunsuk Kang, CMU, USA
- Florent Kirchner, CEA List, France
- Mark Lawford, McMaster, Canada
- Thierry Lecomte, ClearSy, France
- Dominique Mery, LORIA, France 
- Ravi Metta, TCS, India
- Vincent Nimal, Microsoft, USA
- Marco Roveri, FBK, Italy
- Neeraj Singh, ENSEEITH, France

ORGANIZING COMMITTEE:
===
- Fuyuki Ishikawa, National Institute of Informatics, Japan
- 

[TYPES/announce] Call for Participation: Formal Methods in Software Engineering (FormaliSE) (co-located with ICSE 2019)

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CALL FOR PARTICIPATION: FormaliSE 2019 
https://www.formalise.org/ 
Conference on Formal Methods in Software Engineering (May 27th)
co-located with ICSE 2019, Montréal, Canada

INTRODUCTION
FormaliSE is a yearly conference on Formal Methods in Software Engineering. 
FormaliSE is organized by FME (Formal Methods Europe) and is co-located with 
ICSE (International Conference on Software Engineering). The main goal of the 
conference is to foster integration between the formal methods and the software 
engineering communities. The lack of formalization in key places makes software 
engineering overly sensitive to the weaknesses that are inevitable in the 
complex activities behind software creation. This is where formal methods (FMs) 
have a huge opportunity.

The program (https://www.formalise.org/program 
) features presentations of 13 research 
papers. Dr. Jeffrey Joyce (Critical System Labs Inc., Canada) will give a 
keynote presentation. 

VENUE
FormaliSE 2019 will be held at the Fairmont The Queen Elizabeth Hotel, 
Montréal, Canada.

REGISTRATION
Registration for FormaliSE is open. You can register here 
(https://2019.icse-conferences.org/attending/registration 
). Registration is 
handled by ICSE. Early bird registration deadline is 1 April 2019.

ACCOMODATION
A number of hotel rooms have been blocked for ICSE 2019 participants, click 
here (https://2019.icse-conferences.org/attending/hotel-registration 
) for details.

See you in Montréal!

Nico Plat and Stefania Gnesi (General Chairs)
Nancy Day and Matteo Rossi (PC Chairs)

Keynote speaker
Dr. Jeffrey Joyce is the co-founder and managing director of a Vancouver-based 
engineering consultancy, Critical System Labs Inc., (CSL) that provides clients 
with expertise in the specification, analysis and certification of 
software-intensive critical systems. Jeff has more than 30 years of experience 
across a variety of technical domains including aerospace, automotive, defence, 
energy, medical devices and rail signalling systems. He has served on 
international working groups that have developed industry standards such as 
RTCA DO-178C (airborne software), RTCA DO-333 (formal methods) and ISO 26262 
(automotive). In 1990, Jeff earned a doctorate from Cambridge University 
following earlier degrees from the University of Calgary and the University of 
Waterloo. His doctoral research under the supervision of Prof. Michael Gordon 
was among early work on the use of formal methods to verify digital hardware. 
More recently, Jeff and his CSL colleagues have use formal methods to verify 
aspects of critical software systems for clients in aerospace, automotive and 
high-energy physics.

Title of the keynote: The Benefits of (having doubts about) Formal Methods
To believe with certainty we must begin with doubting - Stanisław Leszczyński 
(1677 – 1766)

Abstract: A variety of industry standards for critical systems, such as RTCA 
DO-178C and ISO 26262, refer to the possibility of using formal methods to 
produce verification results for the purpose of certification. However, 
satisfying the expectations of a certification authority using verification 
results obtained by means of formal methods can be a formidable challenge. Dr. 
Joyce will describe some reasonable doubts that might be raised by a 
certification authority about a plan to use formal methods as a source of 
verification results in place of test-based results. He will explain how such 
doubts influenced guidance developed by the aerospace industry for use of 
formal methods in the certification of airborne software. Anticipating these 
doubts can be the basis of an effective strategy to use formal methods as part 
of the certification of a critical system.

[TYPES/announce] Formal verification position at Toyota ITC, Mountain View

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

https://bit.ly/2IOv2WQ?

Connected cars are emerging as a ground for cutting-edge technologies in the 
automotive industry. Communication between cars, other edge devices, and the 
cloud has the potential to support brand-new mobility services and 
sophisticated new technologies, e.g., advanced information sharing, coordinated 
autonomous systems, highly distributed control systems, etc.

With the advent of this new technology trend, a high demand for quality 
assurance of software-centric connected systems arises. Toyota InfoTechnology 
Center, Systems and Software Division is conducting research projects including 
high-assurance connected software architecture, dependable connected software 
platform, system assurance, model-based design and certification.

We are seeking talented candidates for a Senior Researcher involving full-time 
research on high-assurance connected software architecture and advanced 
analytics based on modeling & monitoring of connected cars.

Primary Responsibilities:

Research on High-Assurance Connected Software Architecture including:
oContract-based Architecture, contract-based design, formal contract 
languages;
oAutomatic formal verification;
oRuntime verification and runtime monitoring, verification, and recovery;
oContract-based safety and security analysis;
oContract negotiation;
oCorrectness-by-construction and design-by-contract.

Research on Advanced Analytics Based on Modeling & Monitoring of Connected Cars 
including:
oParametric system modeling & parameter estimation
oContext modeling of connected vehicles and human drivers
oMulti-fidelity modeling
oDigital Twin service architecture

Qualifications:

Ph. D in Computer Science, Electrical Engineering, Computer Engineering, or 
related field.
5+ years of research experience in formal verification and model-based design. 
Industry Experience working in a corporate lab setting with a proven track 
record of cross-functional collaboration and achievements is a plus.

Experience/Skills Required:

Proficiency in formal verification tools, e.g., theorem prover tools, model 
checking tools, etc.
Knowledge of system modeling, formal analysis and parameter estimation.
Knowledge of computer systems, embedded systems, and systems and software 
engineering
Knowledge of programming and scripting languages, e.g., Java, Python, etc.
Excellent research prototype development skills.
Ability to lead a research project, e.g.,  planning, reporting, and managing 
time / team / outside collaborators.
Excellent interpersonal and communication skills

Application:

To apply for this position, please submit your information at the company 
website with the following materials:

A cover letter explaining why you would like to work with us
Latest Resume/CV
Any other information that you think we should consider when reviewing your 
application

About us:

Our mission is changing the experience of mobility, by providing expanded 
options built on innovative research and technology solutions. Our work 
utilizes the resources of vehicles, infrastructure and emergent technologies to 
provide tangible benefits to the public by enabling stress-free mobility of 
people and goods and delivering differentiated experiences through deep 
personalization.

Our current areas of interest include future vehicular networks, in-vehicle 
software and system architecture, vehicle-to-vehicle communication technology, 
and intelligent computing technology including artificial intelligence and 
machine learning.

[TYPES/announce] Formal methods internship at Toyota ITC

[Eunsuk Kang]

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello,

Please forward this e-mail to PhD/Masters students who may be  
interested in doing a summer internship applying formal methods to  
intelligent cars.


Regards,
Eunsuk

==

Summer Intern, Formal Methods for Connected Cars

Application link:

https://careers.jobscore.com/careers/toyotaitc/jobs/summer-intern-formal-methods-for-connected-cars-b-YkXAcTyr6lG5dG1ZS6tF

JOB SUMMARY
Communication between cars, edge, and cloud computing is expected to  
have a great impact on the next generation architecture of car systems  
that opens a new era of mobility. In other words, connected cars are  
emerging as a new foundation of evolution in the automotive industry.


This internship position, Formal Methods for Connected Cars, involves  
performing research and development tasks on methodologies for  
designing safe connected vehicles using formal system modeling and  
verification techniques. In particular, intern will survey and develop  
tools and methods for specifying end-to-end vehicle requirements,  
decomposing high-level requirements into component specifications, and  
automatically verifying that a component satisfies its specification.  
Toyota InfoTechnology Center, Systems and Software Research Team is  
looking for highly self-motivated PhD/Master students in Computer  
Science or related fields to join us in this project.


OBJECTIVES
This project will provide the intern with unique opportunities to  
perform one or more of the following:


Develop a specification language for expressing various types of  
requirements for connected cars, including security, safety, and  
performance,
Develop an automated, scalable verification technique to analyze the  
behavior of software systems for connected cars,
Develop research prototypes and apply them to realistic scenarios in  
connected vehicle interactions,
Collaborate with researchers on publications at top  
conferences/journals, if time permits


QUALIFICATIONS
Currently pursuing a PhD program in computer science or electrical  
engineering,
Experience in formal methods, including formal modeling languages and  
verification techniques (e.g., model checking, constraint solving,  
theorem proving)

Strong background in formal logic and mathematics.
Excellent programming skills (C++, C#, Java), and ability to build  
rapid prototypes.
Familiarity with cyber-security, computer networks, software  
architecture, and cloud computing a plus.
Demonstrated ability to work independently as well as within a highly  
motivated team environment.
Excellent communication skills and a proven ability to deliver on  
challenging software development tasks.

ADMINISTRATIVE DETAILS
1. Part-time (up to 6 months) or full-time (up to 3 months) internship  
in the summer of 2018 at Toyota ITC's Mountain View, CA office.
2. Applicants *must* already have the ability/authorization to work in  
the USA (Toyota ITC will NOT provide VISA support).


To apply for an intern position, please submit your application along  
with the following materials:


CV/Resume
Cover letter explaining your interest in the job and desired time  
frame for the internship.


ABOUT US
Since 2001, Toyota InfoTechnology Center USA, Inc. has specialized in  
R and business research with a focus on cutting-edge information  
technologies to advance the driving experience of Toyota automobiles  
and safety of the automotive industry on the globe. ITC’s current  
areas of interest include future vehicular network, in-vehicle  
software and system architecture, vehicle-to-vehicle communication  
technology, intelligent computing technology including artificial  
intelligence and machine learning.

[TYPES/announce] Workshop on the Future of Alloy

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

---
Call for Participation: Workshop on the Future of Alloy

Location: MIT, Cambridge, MA
Date & duration: April 30 & May 1, 2018
Registration & logistics: http://alloy.mit.edu/workshop
---

The goal of the workshop is to bring together researchers and users of Alloy, 
share their perspectives, and formulate short/long-term agendas for improving 
the language & its tools. Participants from both industry and academia are 
welcome.

We hope to encourage discussions on the following topics (and others, suggested 
by participants):

- Extensions: What’s not so easy to express in Alloy, and what language 
extensions could we make? What are some alternative backends that we could 
explore (e.g., SMT)? 
- Benchmarks: How do we collect and share models built by users over the years? 
What kind of infrastructure do we need?
- Usability: What are some obstacles preventing a wider adoption of Alloy? What 
usability improvements could we make?
- Education: How do we teach Alloy to students and practitioners? What 
education materials could we develop and share among teachers?

Call for presentations: The content of the workshop will be driven largely by 
participants’ ideas about improving Alloy. To stimulate discussion, we are 
soliciting short 10~15 min talks from attendees. Topics for a talk may include 
(but not limited to): Your own positive/negative experiences with Alloy, ideas 
for improvement, a demo of your tool, or calls for community-wide effort. If 
you are interested in giving a talk, please fill out the relevant items in the 
registration form, linked from the workshop website:

http://alloy.mit.edu/workshop

Please share this announcement with other colleagues or students who may also 
be interested in attending the workshop. Looking forward to seeing you at the 
workshop!

Eunsuk Kang, Sarfraz Khurshid, and Emina Torlak (Program co-chairs)
Daniel Jackson (General chair)​

[TYPES/announce] Research position in formal methods for intelligent cars

[Eunsuk Kang]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Please apply using the following link if you are interested:

https://careers.jobscore.com/careers/toyotaitc/jobs/researcher-formal-methods-for-intelligent-connected-cars-ap4ixuCW4r553ydG1ZS6tF

Job Description

Researcher, Design by Contract and Formal Methods for Intelligent Connected Cars

Summary:
Connected cars are emerging as a ground for cutting-edge technologies in the 
automotive industry. Communication between cars, edge, and cloud computing has 
great potential for sophisticated new technologies, e.g., advanced information 
sharing, coordinated autonomous systems, highly distributed control systems, 
etc. With the advent of this new technology trend, a high demand for quality 
assurance for software-centric connected systems arises. Toyota InfoTechnology 
Center is conducting research projects including high-assurance connected 
software architecture, dependable connected software platform, system 
assurance, and certification. 

Toyota InfoTechnology Center, Systems and Software Research Team is seeking 
talented researcher candidates for high-assurance connected software 
architecture projects.

Primary Responsibilities:
Research on High-Assurance Connected Software Architecture including:
— Contract-based architecture, contract-based design, formal contract languages;
- Automatic formal verification;
- Runtime verification and monitoring;
- Correctness-by-construction;
- Automatic abstraction (bottom-up) and decomposition (top-down) of system 
specifications.

Qualifications:
- Ph.D. in Computer Science, Electrical Engineering, Computer Engineering, or 
related field.

Requirements:
- Research experience in formal verification.
- Proficiency in formal verification tools, e.g., theorem prover tools, model 
checking tools, etc. 
- Knowledge of computer systems, embedded systems, and systems and software 
engineering.
- Knowledge of programming and scripting languages, e.g., Java, Python, etc.
- Research prototype development skills.
- Ability to engage in general research activities, e.g.,  planning, time 
management, and team building.
- Ability to work independently as well as within a highly motivated team 
environment.
- Excellent interpersonal and communication skills.

Application:

To apply for this position, please submit your information at the company 
website:

https://careers.jobscore.com/careers/toyotaitc/jobs/researcher-formal-methods-for-intelligent-connected-cars-ap4ixuCW4r553ydG1ZS6tF?ref=rss=68

About Toyota ITC:
Since 2001, Toyota InfoTechnology Center USA, Inc. has specialized in R and 
business research with a focus on cutting-edge information technologies to 
advance the driving experience of Toyota automobiles and safety of the 
automotive industry around the globe. ITC’s current areas of interest include 
future vehicular network, in-vehicle software and system architecture, 
vehicle-to-vehicle communication technology and intelligent computing 
technology.