\documentclass[twoside,english,a4paper,12pt]{article}
%\usepackage{b5}
\RequirePackage[a4paper,top=2cm,left=2cm,right=2cm,bottom=1.5cm,nohead,nofoot]{geometry}
\parindent 0pt
\parskip 0pt
%\parskip 3pt
\usepackage{babel}
\usepackage[latin1]{inputenc}
%\usepackage[utf8]{inputenc}
%\usepackage{fancyvrb}
\usepackage{fancyhdr}
\usepackage{t1enc}
\usepackage{url}
\usepackage{aeguill}
\usepackage{graphicx}
\usepackage{pdfpages}
\usepackage{compact}
%\def\sp{\mbox{}\hspace{8mm}}
\def\sp{}

%% \pagestyle{fancy}
%% \fancyhead[LE,RO]{\small\thepage}
%% \fancyfoot[R,L]{}
%% %\fancyfoot[C]{\today}
%% \fancyfoot[C]{}
%% \renewcommand{\subsectionmark}[1]{\markboth{ \thesubsection.\ #1}{}}
%% \renewcommand{\subsubsectionmark}[1]{\markright{ \thesubsubsection.\ #1}}
%% %\rhead{\nouppercase{\rightmark}}
%% %\lhead{\nouppercase{\leftmark}}
%% \fancyhead[LO]{\nouppercase{\small\rightmark}}
%% \fancyhead[RE]{\nouppercase{\small\leftmark}}
%% %\fancyhead[RE,LO]{}      
\newcommand{\tit}[3]{\noindent\fbox{\begin{minipage}{\textwidth}\begin{center}
{\Huge #1 \\ \huge #2 \\ \large #3\\}
\end{center}\end{minipage}} \mbox{}\\}

\begin{document}

\thispagestyle{empty}
\pagestyle{empty}
\def\thepage{}

\tit{Programme of MBT}{3rd Workshop on Model Based Testing}{March 31, April 1, room: CP2-102}

\subsubsection*{09:00 - 10:30 SESSION 1}

\textbf{Opening and Welcome}
\begin{itemize}
    \item  Bernd Finkbeiner, Yuri Gurevich, Alexander K. Petrenko 
\end{itemize}
\textbf{Invited Talk}
\begin{itemize}
   \item   Finding a Good Order for Applying Adaptive Test Cases 
    Rob Hierons 
\end{itemize}

\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}

\begin{itemize}
  \item    A Global Algorithm for Model-Based Test Suite Generation 
    Anders Hessel and Paul Pettersson 
    \item  Can a Model Checker Generate Tests for Non-Deterministic Systems? 
    Sergiy Boroday, Alexandre Petrenko, and Roland Groz 
\end{itemize}

\subsubsection*{12:30 - 14:30 Lunch}
\subsubsection*{14:30 - 16:00 SESSION 3}

\begin{itemize}
    \item  Generating Scenarios by Multi-Object Checking 
    Maik Kollmann and Yuen Man Hon 
   \item   Testing Planning Domains (without Model Checkers) 
    Franco Raimondi, Charles Pecheur, and Guillaume Brat 
\end{itemize}

\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:15 SESSION 4}

\begin{itemize}
    \item  Towards the Integration of Visual and Formal Models for GUI Testing 
    Ana C. R. Paiva, João C. P. Faria, and Raul F. A. M. Vidal 
\end{itemize}

\subsubsection*{17:15 - 18:00 Reserved}
\subsubsection*{18:45 SOCIAL EVENT}

Joint Workshops Post-Conference Dinner (tickets needed)
    Dinner at Pousada Santa Maria de Bouro 
    Shuttle departure from University Campus, Gualtar 

\subsection*{Sunday, April 1, room: CP2-102}

\subsubsection*{09:00 - 10:30 SESSION 1}

\textbf{Invited Talk}
\begin{itemize}
  \item    Model-Based Testing in the Standardization of Information and Communication Technologies: the ETSI
Perspective 
    Antti Huima 
\end{itemize}

\subsubsection*{10:30 - 11:00 Coffee Breaks}
\subsubsection*{11:00 - 12:30 SESSION 2}

\begin{itemize}
    \item  Measuring a Java Test Suite Coverage using JML Specifications 
    Frédéric Dadeau, Yves Ledru, and Lydie du Bousquet 
   \item   A Case Study in Matching Test and Proof Coverage 
    Lydie du Bousquet, Yves Ledru, Frédéric Dadeau, and Faryel Allouti 

\end{itemize}

\subsubsection*{12:30 - 14:30 Lunch}
\subsubsection*{14:30 - 16:00 SESSION 3}

\begin{itemize}
     \item Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT
Solver 
    Martin Ouimet and Kristina Lundqvist 
  \item    Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers 
    Gordon Fraser, Bernhard K. Aichernig, and Franz Wotawa 
\end{itemize}

\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:15 Discussion}

\end{document}