Naslov
Formalna verifikacija digitalnih sustava temeljena na logičkoj zadovoljivosti
(Formal verification of digital systems based on Boolean satisfiability)

Autori
Ivišić, Robert

Vrsta, podvrsta i kategorija rada
Ocjenski radovi, diplomski rad, preddiplomski

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
12.02

Godina
2010

Stranica
54

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
zadovoljivost; SAT; DPLL; MiniSAT
(satisfiability; SAT; DPLL; MiniSAT)

Sažetak
Suvremeni alati za formalnu verifikaciju digitalnih sustava sadrže postupak rješavanja problema odlučivanja koji se sastoji u dokazivanju da li se formula propozicijske logike može zadovoljiti nekom supstitucijom vrijednosti varijabli (tzv. SAT problem). U radu je potrebno objasniti ulogu SAT podsustava u verifikaciji programskih produkata. Na temelju implementiranog sustava otvorenog koda za rješavanje SAT problema pokazati njegovu uporabu i djelotvornost u postupku formalne verifikacije. Primjenu proširiti na po volji odabrani problem koji sadrži konfliktna ograničenja.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA