|
|
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (vedoucí práce) ; Metcalfe, George (oponent) ; Ramanayake, Revantha (oponent)
Důkazové systémy: forma a složitost Tato disertační práce obsahuje tři části. První dvě části spolu souvisí. V [1] a [2], Iemhoff objevila souvislost mezi existencí terminujícího sekvenčního kalkulu určitého druhu a uniformní interpolační vlastností superintuicioni- stické logiky, kterou tento kalkulus zachycuje. Ve druhé části budeme tento vztah zobecňovat tak, aby pokrýval také substrukturální nastavení na jedné straně a silnější typ systémů nazývaných semi-analytické kalkuly na straně druhé. Abychom byli přesnější, ukážeme, že jakákoli dostatečně silná sub- strukturální logika se semi-analytickým kalkulem má Craigovu interpolační vlastnost a v případě, že je kalkulus terminující, má uniformní interpo- laci. Tento vztah pak vede k některým konkrétním aplikacím. Pozitivním výsledkem je, že poskytuje jednotnou metodu k prokázání uniformní in- terpolační vlastnosti pro logiky FLe, FLew, CFLe, CFLew, IPC, CPC a některá z jejich modálních rozšíření K a KD. Další aplikací je nega- tivní výsledek, že mnohé substrukturální logiky, včetně Ln, Gn, BL, R a RMe , téměř všechny superintuicionistické logiky (kromě nejvýše sedmi z nich) a téměř všechna rozšíření S4 (kromě třiceti sedmi z nich)...
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (vedoucí práce) ; Gargantini, Angelo (oponent) ; Barnat, Jiří (oponent)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (vedoucí práce) ; Gargantini, Angelo (oponent) ; Barnat, Jiří (oponent)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Methods for reduction of Craig's interpolant size using partial variable assignment
Blicha, Martin ; Kofroň, Jan (vedoucí práce) ; Kučera, Petr (oponent)
V čase, ktorý ubehol od prvého použitia interpolantov v oblasti symbolického overovania modelov (symbolic model checking), sa metódy založené na interpolantoch s úspechom uplatnili v oblasti overovania hardvéru aj softvéru. Prednedávnom sa v oblasti výpočtu interpolantov objavili čiastočné ohodnotenia premenných. V kontexte takzvaných "abstract reachability graphs" predstavujú čiatočné ohodnotenia spôsob ako sa zároveň elegantne vysporiadať s premennými mimo aktuálny kontext a zároveň dosiahnuť zmenšenie spočítaného interpolantu. V tejto práci sme ďalej rozvinuli systém pre počítanie interpolantov za prítomnosti čiastočných ohodnotení, dokázali sme jeho korektnosť a ukázali sme jeho potenciál pre ďalšie zmenšenie počítaných interpolantov. Nakoniec sme analyzovali za akých podmienok budú mať počítané interpolanty vlastnosť dôležitú pre mnoho techník založených na interpolácií - tzv. path interpolation property. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.