Algorithms for Context-Aided Variable Elimination

Inigo Incer, Albert Benveniste, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2023-15
January 28, 2023

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.pdf

Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or abstractions of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and abstractions of linear inequality constraints.


BibTeX citation:

@techreport{Incer:EECS-2023-15,
    Author = {Incer, Inigo and Benveniste, Albert and Murray, Richard M. and Sangiovanni-Vincentelli, Alberto L. and Seshia, Sanjit A.},
    Title = {Algorithms for Context-Aided Variable Elimination},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2023},
    Month = {Jan},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.html},
    Number = {UCB/EECS-2023-15},
    Abstract = {Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system.
This paper presents algorithms for eliminating variables from formulas by computing refinements or abstractions of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and abstractions of linear inequality constraints.}
}

EndNote citation:

%0 Report
%A Incer, Inigo
%A Benveniste, Albert
%A Murray, Richard M.
%A Sangiovanni-Vincentelli, Alberto L.
%A Seshia, Sanjit A.
%T Algorithms for Context-Aided Variable Elimination
%I EECS Department, University of California, Berkeley
%D 2023
%8 January 28
%@ UCB/EECS-2023-15
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.html
%F Incer:EECS-2023-15