ERROR:SQLSTATE[HY000]: General error: 20018 Invalid column name 'CodigoInstitucion'. [20018] (severity 16) [SELECT PublicObrasAutores.NumeroEmpleado, PublicObrasAutores.ApellidoPaterno, PublicObrasAutores.ApellidoMaterno, PublicObrasAutores.Nombre, PublicObrasAutores.NombreCompleto FROM PublicObrasAutores LEFT JOIN PublicObrasAutoresFil ON PublicObrasAutores.RefPublicacion = PublicObrasAutoresFil.RefPublicacion WHERE PublicObrasAutores.RefPublicacion = '569410' AND PublicObrasAutores.NumeroEmpleado IS NULL AND PublicObrasAutoresFil.CodigoInstitucion IS NOT NULL;]
SELECT PublicObrasAutores.NumeroEmpleado, PublicObrasAutores.ApellidoPaterno, PublicObrasAutores.ApellidoMaterno, PublicObrasAutores.Nombre, PublicObrasAutores.NombreCompleto FROM PublicObrasAutores LEFT JOIN PublicObrasAutoresFil ON PublicObrasAutores.RefPublicacion = PublicObrasAutoresFil.RefPublicacion WHERE PublicObrasAutores.RefPublicacion = '569410' AND PublicObrasAutores.NumeroEmpleado IS NULL AND PublicObrasAutoresFil.CodigoInstitucion IS NOT NULL;

ERROR:SQLSTATE[HY000]: General error: 20018 Invalid column name 'CodigoInstitucion'. [20018] (severity 16) [SELECT PublicObrasAutores.NumeroEmpleado, PublicObrasAutores.ApellidoPaterno, PublicObrasAutores.ApellidoMaterno, PublicObrasAutores.Nombre, PublicObrasAutores.NombreCompleto FROM PublicObrasAutores LEFT JOIN PublicObrasAutoresFil ON PublicObrasAutores.RefPublicacion = PublicObrasAutoresFil.RefPublicacion WHERE PublicObrasAutores.RefPublicacion = '569410' AND PublicObrasAutores.NumeroEmpleado IS NULL AND PublicObrasAutoresFil.CodigoInstitucion IS NULL;]
SELECT PublicObrasAutores.NumeroEmpleado, PublicObrasAutores.ApellidoPaterno, PublicObrasAutores.ApellidoMaterno, PublicObrasAutores.Nombre, PublicObrasAutores.NombreCompleto FROM PublicObrasAutores LEFT JOIN PublicObrasAutoresFil ON PublicObrasAutores.RefPublicacion = PublicObrasAutoresFil.RefPublicacion WHERE PublicObrasAutores.RefPublicacion = '569410' AND PublicObrasAutores.NumeroEmpleado IS NULL AND PublicObrasAutoresFil.CodigoInstitucion IS NULL;

ERROR:SQLSTATE[HY000]: General error: 20018 Invalid column name 'Institucion'. [20018] (severity 16) [SELECT Institucion FROM PublicObrasAutoresFil WHERE RefPublicacion = '569410']
SELECT Institucion FROM PublicObrasAutoresFil WHERE RefPublicacion = '569410'

ERROR:SQLSTATE[HY000]: General error: 20018 Invalid column name 'Institucion'. [20018] (severity 16) [SELECT Institucion FROM PublicObrasAutoresFil WHERE RefPublicacion = 569410 AND InstitucionPropia = 'S' UNION SELECT Adscripciones.Entidad FROM PublicacionesObras JOIN PublicObrasAutores ON PublicacionesObras.Identificador = PublicObrasAutores.RefPublicacion JOIN Adscripciones ON PublicObrasAutores.NumeroEmpleado = Adscripciones.NumeroEmpleado WHERE (PublicacionesObras.FechaPublicacion BETWEEN Adscripciones.FechaDesde AND Adscripciones.FechaHasta OR (PublicacionesObras.FechaPublicacion >= Adscripciones.FechaDesde AND Adscripciones.FechaHasta IS NULL)) AND PublicacionesObras.Identificador= 569410]
SELECT Institucion FROM PublicObrasAutoresFil WHERE RefPublicacion = 569410 AND InstitucionPropia = 'S' UNION SELECT Adscripciones.Entidad FROM PublicacionesObras JOIN PublicObrasAutores ON PublicacionesObras.Identificador = PublicObrasAutores.RefPublicacion JOIN Adscripciones ON PublicObrasAutores.NumeroEmpleado = Adscripciones.NumeroEmpleado WHERE (PublicacionesObras.FechaPublicacion BETWEEN Adscripciones.FechaDesde AND Adscripciones.FechaHasta OR (PublicacionesObras.FechaPublicacion >= Adscripciones.FechaDesde AND Adscripciones.FechaHasta IS NULL)) AND PublicacionesObras.Identificador= 569410

Título del libro: 2020 8th Edition Of The International Conference In Software Engineering Research And Innovation (conisoft 2020)
Título del capítulo: Formal Verification of a Database Management System

Autores UNAM:
DIEGO ROBERTO MEDINA MARTINEZ; ISMAEL EVERARDO BARCENAS PATIÃ?O; GUILLERMO GILBERTO MOLERO CASTILLO; ALEJANDRO VELAZQUEZ MENA; ROCIO ALEJANDRA ALDECO PEREZ; SERGIO JOAQUIN JIMENEZ SANDOVAL; HANNA JADWIGA OKTABA;

---

Autores externos:

---

Idioma:

---

Año de publicación:
2020

---

Palabras clave:

Program Verification; Separation logic; Database Management Systems

---

Resumen:

Assertion based program verification is a well-known formal approach to (dis)prove correctness of algorithms associated to software systems. Assertions are input and output properties a correct program must satisfy. These properties are traditionally written in a specification language based on classical logic. Associated classical reasoning (inference) systems are then used to (dis)prove program correctness. However, when programs manipulate mutable data structures such as pointers, classical logical operators have been unable to successfully model syntactically unrelated expressions. In this article, we study separation logics, which are equipped with specially-purposed operators to model mutable data structures. We describe the use of this logic as a specification language in the verification of a database management system (DMS). In particular, we detect several bugs in two DMS libraries regarding heap manipulation. We describe these bugs in detail and propose solutions.

---

Entidades citadas de la UNAM:

---

Fuente:



ISBN:
9781728184500
Editorial:
IEEE COMPUTER SOC

Tipo de producto:
Proceedings Paper

DOI:
10.1109/CONISOFT50191.2020.00024