dual license Apache-2.0 and BSD-3-Clause

COPYRIGHT

@@ -0,0 +1,6 @@
+SPDX-License-Identifier: Apache-2.0 OR BSD-3-Clause
+
+HOL4P4 is licensed under the the Apache License, Version 2.0
+<LICENSE-APACHE> or <http://www.apache.org/licenses/LICENSE-2.0>, or
+the BSD 3-Clause License <LICENSE-BSD> or
+<https://spdx.org/licenses/BSD-3-Clause.html>, at your option.

LICENSE.md → LICENSE-APACHE

@@ -186,7 +186,7 @@
       same "printed page" as the copyright notice for easier
       identification within third-party archives.
 
-   Copyright 2022 Didrik Lundberg, Anoud Alshnakat, Roberto Guanciale, Mads Dam, Karl Palmskog, Arve Gengelbach
+   Copyright 2022-2025 Didrik Lundberg, Anoud Alshnakat, Roberto Guanciale, Mads Dam, Karl Palmskog, Arve Gengelbach
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.

LICENSE-BSD

@@ -0,0 +1,32 @@
+HOL4P4 COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.
+
+Copyright 2022-2025 by the HOL4P4 CONTRIBUTORS
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * The names of the copyright holders and contributors may not be
+    used to endorse or promote products derived from this software
+    without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS
+OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR
+TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
+USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.

README.md

@@ -69,3 +69,9 @@ To set up the development environment, follow the instructions in [INSTALL.md](I
 A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane", in P4 Workshop in Europe (EuroP4 '22), 2022.
 
 A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4", to appear in (OOPSLA '24).
+
+## License
+
+This project is distributed under the terms of the Apache License (Version 2.0), and the BSD 3-Clause License; users may pick which license to apply.
+
+See [`COPYRIGHT`](COPYRIGHT), [`LICENSE-APACHE`](LICENSE-APACHE) and [`LICENSE-BSD`](LICENSE-BSD) for details.