JML Workshop: UCF in Orlando Florida, December 18-19, 2017


Meetings will start at 9am and run until about 5pm on December 18 and 19, 2017 in the Garden Room of the UCF Live Oak Center.

You can walk to the Live Oak Center using the linked map. On the UCF Campus map the intersection of Alafaya Trail and University Drive, where you would enter the University campus on foot, is near A10. The Live Oak Center is between E9 and F9. If you drive there, you can park in Garage B, which is just south of the Live Oak Center (between E9 and E10 on the campus map), and pay $5 per day to the machines located near the stairwells for parking your car.

Note that breakfast and dinners are on your own.

A tentative schedule for the meeting, which will be updated dynamically, is as follows. Please let Gary Leavens ( know the exact title of your talk and if you will be able to be ready when it is scheduled (or not).

Date Time Speaker Title/Subject
Dec. 18 9 AM - 9:30 AM   Coffee and Introductions
Dec. 18 9:30 AM - 10:30 AM Daniel Zimmerman Verification at Galois
Dec. 18 10:30 AM - 11:30 AM Nikolai Kosmatov Specification and proof of relational properties with Frama-C
Dec. 18 11:30 AM - noon   Discussion
Dec. 18 noon - 1:00 PM   Lunch (provided)
Dec. 18 1:00 PM - 2:00 PM Werner Dietl Preventing Errors before they Happen: The Checker Framework
Dec. 18 2:00 PM - 2:30 PM   Break
Dec. 18 2:30 PM - 3:30 PM Henrique Rebelo AspectJML
Dec. 18 3:30 PM - 4:00 PM   Discussion
Dec. 18 4:00 PM - 5:00 PM   Semantics of JML
Dec. 19 9 AM - 9:30 AM   Coffee
Dec. 19 9:30 AM - 10:30 AM John Singleton Strongarm: An Approach to Inferring Practical Postconditions
Dec. 19 10:30 AM - 11:30 AM Yuyan Bao Frame Constraints for Behavioral Subtyping
Dec. 19 11:30 AM - noon   Discussion
Dec. 19 noon - 1:00 PM   Lunch (provided)
Dec. 19 1:00 PM - 2:00 PM David Cok Lessons Learned (and future work) from a real-world Java verification project
Dec. 19 2:00 PM - 2:30 PM   Break
Dec. 19 2:30 PM - 3:30 PM Mattias Ulbrich Proving Relational Properties Using JML and KeY
Dec. 19 3:30 PM - 4:00 PM Luke Myers ProVerif to JML Compiler
Dec. 19 4:00 PM - 5:00 PM Wytse H. M. Oortwijn Verifying Concurrent Programs with VerCors


Please email Gary T. Leavens ( to reserve your place at the meeting by November 27, 2017. Please include an indication of what you would like to talk about at the workshop.


Aside from travel and the hotel (see below), the workshop will charge about $10 per person for computer projection equipment and $36 per person for two lunches. So the total cost payable to the organizers is estimated to be about $46 per participant. Participants should plan to pay on their own for other meals (breakfast and dinner).


We have a special rate in the DoubleTree by Hilton Orlando East - UCF Area of $99 per night (excluding taxes). The rate includes free wi-fi access. Recreational amenities at the hotel include an outdoor pool and a fitness center.

Please use the booking link, which is, to reserve a room. Use the group code "JML" (without the quotes). The rate should work for an arrival of December 17 or December 18 and leaving by December 19.

If you reserve a room by phone (+1 855-213-0582), mention the group name: "UCF Department of Computer Science - JML Workshop" to get the special rate.

Travel to Orlando


The closest airport is the Orlando International Airport (MCO). This airport is served by a large number of carriers. It also offers free Wi-Fi service.

From the Orlando International Airport (MCO) to the Hotel

By Taxi

If you want to take a taxi, proceed to the taxi stand. There are two taxi stands:

The rate to the conference hotel will be about $52 (estimate $57 with a tip). Taxis may carry up to 9 passengers, and charge the same rate regardless of the number of passengers. All taxicabs picking up at the Airport are regulated by the City of Orlando's Vehicle-for-Hire ordinance which requires fares to be determined by a taximeter.

Flat rate fees are not authorized. Therefore metered rate may vary from the approximate rates quoted above.

More information and numbers of taxi services is available from the MCO website.

By Automobile: Renting a Car

Rental car companies are located on the A-Side and B-Side of the Terminal on the Ground Transportation Level (Level 1). The MCO website has more information and links to the rental car companies.

Last modified Friday, December 10, 2021.