This paper presents an approach for designing correct-by-construction Autonomous Intersection Management (AIM) algorithms for autonomous vehicles using formal methods. The task of the AIM is to establish the right-of-way (priorities) for the incoming autonomous vehicles. Based on the assumption that the vehicles communicate their planned paths, namely the entering and the exiting points of the intersection, e.g., over V2I protocol, the AIM makes sure that the trajectories of the incoming vehicles do not overlap. We argue that traffic efficiency and flow can be increased with an intelligent algorithm; however, the safety of this algorithm should be verified formally and then tested in a simulation environment. In this paper, we use formal methods for synthesizing a control protocol with safety guarantees. The intersection and the incoming vehicles are modeled as transition systems; their composition constitutes the overall concurrent system. The control protocol is synthesized using a set of specifications (safety properties) written in Linear Temporal Logic (LTL). These LTL specifications are then converted to Biichi automata, and the product automaton with the concurrent system results in a new transition system verified by model-checking. Formal verification is complemented by simulation-based tests conducted in MOBATSim (Model-based Autonomous Traffic Simulation Framework). This approach increases the validation envelope for the correct behavior of the system and the validity of the assumptions made for modeling. The synthesis algorithms developed for MATLAB implementation are also published as an open-source library with documentation and case studies.